Renamed DOF_mkroot to mkroot_DOF.

README.md

@@ -86,9 +86,9 @@ editor.
 The DOF-plugin provides an alternative to Isabelle's ``mkroot`` command.
 Isabelle projects that use DOF need to be created using
 ```console 
-foo@bar:~$ isabelle DOF_mkroot 
+foo@bar:~$ isabelle mkroot_DOF 
 ```
-The ``DOF_mkroot`` command takes the same parameter as the standard
+The ``mkroot_DOF`` command takes the same parameter as the standard
 ``mkroot`` command of Isabelle. Thereafter, the normal Isabelle 
 command for building documents can be used. 
 
@@ -96,9 +96,9 @@ Using the ``-o`` option, different ontology setups can be
 selected and using the ``-t`` option, different LaTeX setups 
 can be selected (use ``-h`` to obtain a list of all installed setups):
 ```console 
-foo@bar:~$ isabelle DOF_mkroot -h
+foo@bar:~$ isabelle mkroot_DOF -h
 
-Usage: isabelle DOF_mkroot [OPTIONS] [DIR]
+Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
 
   Options are:
     -h           print this help text and exit
@@ -118,7 +118,7 @@ Usage: isabelle DOF_mkroot [OPTIONS] [DIR]
 ```
 For example, 
 ```console 
-foo@bar:~$ isabelle DOF_mkroot -o scholarly_paper -t lncs
+foo@bar:~$ isabelle mkroot_DOF -o scholarly_paper -t lncs
 ```
 creates a setup using the scholarly_paper ontology and Springer's
 LNCS LaTeX class as document class. Note that the generated setup

examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy

@@ -230,7 +230,7 @@ enforcing a sequence of text-elements that must belong to the corresponding clas
 To start using \isadof, one creates an Isabelle project (with the name 
 \inlinebash{IsaDofApplications}):
 \begin{bash}
-  isabelle DOF_mkroot -o scholarly_paper -t lncs -d  IsaDofApplications
+  isabelle mkroot_DOF -o scholarly_paper -t lncs -d  IsaDofApplications
 \end{bash}
 where the \inlinebash{-o scholarly_paper} specifies the ontology for writing scientific articles and 
 \inlinebash{-t lncs} specifies the use of Springer's \LaTeX-configuration for the Lecture Notes in 

examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy

@@ -14,31 +14,38 @@ cases on aspects of the modeling due to space limitations.\<close>
 
 
 
-section*[install::technical]\<open>Getting Started\<close>
+section*[getting_started::technical]\<open>Getting Started\<close>
+
+subsection*[installation::technical]\<open>Installing \isadof\<close>
+
+subsubsection*[prereq::technical]\<open>Installing \isadof\<close>
+text\<open>You need to have Isabelle \isabelleversion, which can be downloaded ....\<close>
+
+subsection*[first_project::technical]\<open>Creating an \isadof Project\<close>
+
+text\<open>\url{\isadofarchiveurl}\<close>
+
 text\<open>
-
-DOWNLOAD INFO MISSING
-
-INSTALLATION INFO MISSING
-
-CREATING A PROJECT:
-
 To start using \isadof, one creates an Isabelle project (with the name 
 \inlinebash{IsaDofApplications}):
 \begin{bash}
-  isabelle DOF_mkroot -o scholarly_paper -t lncs -d  IsaDofApplications
+ë\prompt{}ë tar xf ë\href{\isadofarchiveurl}{\isadofarchiven}ë
+ë\prompt{}ë cd ë\isadofdirnë
+ë\prompt{\isadofdirn}ë ./install 
+  isabelle mkroot_DOF -o scholarly_paper -t lncs -d  IsaDofApplications
 \end{bash}
 where the \inlinebash{-o scholarly_paper} specifies the ontology for writing scientific articles and 
 \inlinebash{-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:
 \begin{bash}
-  isabelle build -d . IsaDofApplications
+ë\prompt{\isadofdirn}ë  isabelle build -d . IsaDofApplications
 \end{bash}
 \<close>
 
 
-section*[scholar_onto::example]\<open> The Scholar Paper Scenario: Eating One's Own Dog Food. \<close>  
+section\<open>Using Document Ontologies\<close>
+subsection*[scholar_onto::example]\<open>Academic Publications (scholarly\_paper)\<close>  
 text\<open> The following ontology is a simple ontology modeling scientific papers. In this 
 \isadof application scenario, we deliberately refrain from integrating references to
 (Isabelle) formal content in order  demonstrate that \isadof is not a framework from 
@@ -180,7 +187,7 @@ such as @{docitem_ref \<open>fig_figures\<close>}.
 \<close>
      
 
-section*[cenelec_onto::example]\<open> The Certification Scenario following CENELEC \<close>
+subsection*[cenelec_onto::example]\<open>Documents for Certifiations (CENELEC\_50128)\<close>
 text\<open> Documents to be provided in formal certifications (such as CENELEC
 50126/50128, the DO-178B/C, or Common Criteria) can much profit from the control of ontological consistency: 
 a lot of an evaluators work consists in tracing down the links from requirements over 
@@ -251,7 +258,7 @@ doc_class srac = ec  +
 \end{isar}
 \<close>
 
-section*[math_exam::example]\<open> The Math-Exam Scenario \<close> 
+subsection*[math_exam::example]\<open> The Math-Exam Scenario \<close> 
 text\<open> The Math-Exam Scenario is an application with mixed formal and 
 semi-formal content. It addresses applications where the author of the exam is not present 
 during the exam and the preparation requires a very rigorous process, as the french 

examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy

@@ -710,7 +710,7 @@ The general process as such is straight-forward:
   in config files and also will be shown in the help text
   shown by executing 
 
-      \<^verbatim>\<open>isabelle DOF_mkroot -h\<close>
+      \<^verbatim>\<open>isabelle mkroot_DOF -h\<close>
 
 \<^enum> Edit the new template as necessary (using the provided 
   example from the target class as reference):
@@ -730,7 +730,7 @@ The general process as such is straight-forward:
 
 \<^enum> Now the new template should be available, you can check this  with 
  
-     \<^verbatim>\<open>isabelle DOF_mkroot -h\<close>
+     \<^verbatim>\<open>isabelle mkroot_DOF -h\<close>
 
 \<^enum> Create an "tiny/empty" Isabelle project using the ontology "core"
   and test your template. If everything works, celebrate. If it does