diff --git a/Isabelle_DOF-Example-I/IsaDofApplications.thy b/Isabelle_DOF-Example-I/IsaDofApplications.thy index 476c3715..59015688 100644 --- a/Isabelle_DOF-Example-I/IsaDofApplications.thy +++ b/Isabelle_DOF-Example-I/IsaDofApplications.thy @@ -310,15 +310,6 @@ While document classes and their inheritance relation structure meta-data of tex in an object-oriented manner, monitor classes enforce structural organization of documents via the language specified by the regular expression enforcing a sequence of text-elements that must belong to the corresponding classes. - -To start using \<^isadof>, one creates an Isabelle project (with the name -@{boxed_bash \IsaDofApplications\}): -@{boxed_pdf [display]\isabelle dof_mkroot -o scholarly_paper -t lncs IsaDofApplications\} -where the @{boxed_bash \-o scholarly_paper\} specifies the ontology for writing scientific articles and -@{boxed_bash \-t lncs\} specifies the use of Springer's \<^LaTeX>-configuration for the Lecture Notes in -Computer Science series. The project can be formally checked, including the generation of the -article in PDF using the following command: -@{boxed_pdf [display]\isabelle build -d . IsaDofApplications\} \ section*[ontomod::text_section]\ Modeling Ontologies in \<^isadof> \