Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Fixed spacing in front of index entries..

This commit is contained in:
Achim D. Brucker 2021-01-19 23:12:58 +00:00
parent fc2817db0d
commit a9737762fd
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
examples/technical_report/Isabelle_DOF-Manual/02_Background.thy
View File

@ -56,9 +56,9 @@ support for higher specification constructs were built.\<close>
section*[dof::introduction]\<open>The Document Model Required by \<^dof>\<close>
text\<open>
In this section, we explain the assumed document model underlying our Document Ontology Framework
(\<^dof>) in general. In particular we discuss the concepts \<^emph>\<open>integrated document\<close>
\<^bindex>\<open>integrated document\<close>, \<^emph>\<open>sub-document\<close>, \<^bindex>\<open>sub-document\<close>,
\<^emph>\<open>text-element\<close> \<^bindex>\<open>text-element\<close> and \<^emph>\<open>semantic macros\<close> \<^bindex>\<open>semantic macros\<close> occurring
(\<^dof>) in general. In particular we discuss the concepts
\<^emph>\<open>integrated document\<close>\<^bindex>\<open>integrated document\<close>, \<^emph>\<open>sub-document\<close>\<^bindex>\<open>sub-document\<close>,
\<^emph>\<open>text-element\<close>\<^bindex>\<open>text-element\<close>, and \<^emph>\<open>semantic macros\<close>\<^bindex>\<open>semantic macros\<close> occurring
inside text-elements. Furthermore, we assume two different levels of parsers
(for \<^emph>\<open>outer\<close> and \<^emph>\<open>inner syntax\<close>) where the inner-syntax is basically a typed \<open>\<lambda>\<close>-calculus
and some Higher-order Logic (HOL)\<^bindex>\<open>HOL\<close>.