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