Proof reading.

Isabelle_DOF/document/preamble.tex

@@ -121,5 +121,6 @@ France, and therefore granted with public funds of the Program ``Investissements
   \expandafter\index\expandafter{\expanded{#2 (#1)}}%
 }%
 
-
+\sloppy
+\raggedbottom
 \AtBeginDocument{\isabellestyle{literal}\newcommand{\lstnumberautorefname}{Line}}

Isabelle_DOF/thys/manual/M_03_GuidedTour.thy

@@ -30,14 +30,13 @@ section*[getting_started::technical]\<open>Getting Started\<close>
 
 subsection*[installation::technical]\<open>Installation\<close>
 text\<open>
-  In this section, we will show how to install \<^isadof> and its pre-requisites: Isabelle and 
+  In this section, we will show how to install \<^isadof>. We assume a basic familiarity with a 
-  \<^LaTeX>. We assume a basic familiarity with a Linux/Unix-like command line (i.e., a shell). 
+  Linux/Unix-like command line (i.e., a shell). 
-  Furthermore, we focus on the installation of the latest official release of  \<^isadof> as 
+  We focus on the installation of the latest official release of  \<^isadof> as 
   available in the Archive of Formal Proofs (AFP).\<^footnote>\<open>If you want to work with the development version 
   of \<^isadof>, please obtain its source code from the \<^isadof> Git repostitory 
   (\<^url>\<open>https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF\<close> and follow the instructions
   in provided \<^verbatim>\<open>README.MD\<close> file.\<close>
-
   \<^isadof> requires Isabelle\<^bindex>\<open>Isabelle\<close> with a recent \<^LaTeX>-distribution
   (e.g., Tex Live 2022 or later).    
 \<close>
@@ -55,14 +54,13 @@ full qualified path.
 \<close>
 
 text\<open>
-Furthermore, download the latest version of the AFP from \<^url>\<open>https://www.isa-afp.org/download/\<close> and 
+Next, download the the AFP from \<^url>\<open>https://www.isa-afp.org/download/\<close> and 
 follow the instructions given at \<^url>\<open>https://www.isa-afp.org/help/\<close> for installing the AFP as an 
 Isabelle component.\<close>
 
 paragraph\<open>Installing \<^TeXLive>.\<close>
 text\<open>
-  Modern Linux distribution will allow you to install \<^TeXLive> using their respective package 
+ On a Debian-based Linux system (\<^eg>, Ubuntu), the following command 
-  managers. On a modern Debian system or a Debian derivative (\<^eg>, Ubuntu), the following command 
   should install all required \<^LaTeX> packages:
 @{boxed_bash [display]\<open>ë\prompt{}ë sudo aptitude install texlive-full\<close>}
 \<close>
@@ -76,19 +74,17 @@ is currently consisting out of three AFP entries:
   contains the \<^isadof> system itself, including the \<^isadof> manual.
 \<^item> \<^verbatim>\<open>Isabelle_DOF-Example-I\<close>: This entry contains an example of 
   an academic paper written using the \<^isadof> system oriented towards an 
-  introductory paper. The text is based on the CICM 2018 paper~@{cite "brucker.ea:isabelle-ontologies:2018"};
+  introductory paper. The text is based on~@{cite "brucker.ea:isabelle-ontologies:2018"};
   in the document, we deliberately  refrain from integrating references to formal content in order 
-  to demonstrate that \<^isadof> is not a framework from Isabelle users to Isabelle users only, but 
+  to demonstrate that \<^isadof> can be used for writing documents with very little direct use of
-  people just avoiding as much as possible \<^LaTeX> notation.
+ \<^LaTeX>.
 \<^item> \<^verbatim>\<open>Isabelle_DOF-Example-II\<close>: This entry contains another example of 
-  a mathematics-oriented academic paper. It is based on the iFM 2020 paper~@{cite "taha.ea:philosophers:2020"}.
+  a mathematics-oriented academic paper. It is based on~@{cite "taha.ea:philosophers:2020"}.
   It represents a typical mathematical text, heavy in definitions with complex  mathematical notation 
   and a lot of non-trivial cross-referencing  between statements, definitions and proofs which 
   are ontologically tracked. However, wrt. the possible linking between the underlying formal theory 
   and this mathematical presentation, it follows a pragmatic path without any ``deep'' linking to 
-  types, terms and theorems, and therefore does deliberately not exploit \<^isadof> 's full potential.
+  types, terms and theorems, and therefore does deliberately not exploit \<^isadof> 's full potential.\<close>
-
-It is recommended to follow the structure these examples.\<close>
 
 
 section*[writing_doc::technical]\<open>Writing Documents\<close>
@@ -107,27 +103,18 @@ session example = Isabelle_DOF +
   options [document = pdf, document_output = "output", document_build = dof]
 (*theories [document = false]
     A
-    B
   theories
-    C
+    B*)
-    D*)
 \end{config}
 
 The document template and ontology can be selected as follows:
 @{boxed_theory_text [display]
 \<open>
-theory
+theory C imports Isabelle_DOF.technical_report Isabelle_DOF.scholarly_paper begin
-  C
+  list_templates
-imports
+  use_template "scrreprt-modern"
-  Isabelle_DOF.technical_report
+  list_ontologies
-  Isabelle_DOF.scholarly_paper
+  use_ontology "technical_report" and "scholarly_paper"
-begin
-
-list_templates
-use_template "scrreprt-modern"
-list_ontologies
-use_ontology "technical_report" and "scholarly_paper"
-
 end
 \<close>}
 
@@ -161,7 +148,6 @@ session example = HOL +
   options [document = pdf, document_output = "output", document_build = dof]
   session 
     Isabelle_DOF.scholarly_paper
-    Isabelle_DOF.technical_report
   theories
     C
 \end{config}
@@ -308,10 +294,10 @@ which is written in the so-called free-form style: Formulas are superficially pa
 type-set, but no deeper type-checking and checking with the underlying logical context
 is undertaken. \<close>
 
-figure*[fig0::figure,relative_width="90",file_src="''figures/header_CSP_source.png''"]
+figure*[fig0::figure,relative_width="85",file_src="''figures/header_CSP_source.png''"]
        \<open> A mathematics paper as integrated document source ... \<close>  
 
-figure*[fig0B::figure,relative_width="90",file_src="''figures/header_CSP_pdf.png''"]
+figure*[fig0B::figure,relative_width="85",file_src="''figures/header_CSP_pdf.png''"]
        \<open> ... and as corresponding \<^pdf>-output. \<close>  
 
 text\<open>The integrated source of this paper-excerpt is shown in \<^figure>\<open>fig0\<close>, while the
@@ -445,15 +431,15 @@ defined by \<^typ>\<open>article\<close>.
 text*[exploring::float, 
       main_caption="\<open>Exploring text elements.\<close>"]
 \<open>
-@{fig_content (width=48, caption="Exploring a reference of a text-element.") "figures/Dogfood-II-bgnd1.png"
+@{fig_content (width=45, caption="Exploring a reference of a text-element.") "figures/Dogfood-II-bgnd1.png"
-}\<^hfill>@{fig_content (width=47, caption="Exploring the class of a text element.") "figures/Dogfood-III-bgnd-text_section.png"} 
+}\<^hfill>@{fig_content (width=45, caption="Exploring the class of a text element.") "figures/Dogfood-III-bgnd-text_section.png"} 
 \<close>
 
 text*[hyperlinks::float, 
       main_caption="\<open>Navigation via generated hyperlinks.\<close>"]
 \<open>
-@{fig_content (width=48, caption="Hyperlink to class-definition.") "figures/Dogfood-IV-jumpInDocCLass.png"
+@{fig_content (width=45, caption="Hyperlink to class-definition.") "figures/Dogfood-IV-jumpInDocCLass.png"
-}\<^hfill>@{fig_content (width=47, caption="Exploring an attribute (hyperlinked to the class).") "figures/Dogfood-V-attribute.png"} 
+}\<^hfill>@{fig_content (width=45, caption="Exploring an attribute (hyperlinked to the class).") "figures/Dogfood-V-attribute.png"} 
 \<close>
 
 text\<open> 
@@ -498,16 +484,14 @@ text\<open>The present version of \<^isadof> is the first version that supports
 \<^dof>-generated term-antiquotations\<^bindex>\<open>term-antiquotations\<close>, \<^ie>, antiquotations embedded
 in HOL-\<open>\<lambda>\<close>-terms possessing arguments that were validated in the ontological context.
 These \<open>\<lambda>\<close>-terms may occur in definitions, lemmas, or in values to define attributes 
-in class instances. They have the format:\<close>
+in class instances. They have the format: \<open>@{name arg\<^sub>1 ... arg\<^sub>n\<^sub>-\<^sub>1} arg\<^sub>n\<close>\<close>
-
-text\<open>\<^center>\<open>\<open>@{name arg\<^sub>1 ... arg\<^sub>n\<^sub>-\<^sub>1} arg\<^sub>n\<close>\<close>\<close>
 
 text\<open>Logically, they are defined as an identity in the last argument \<open>arg\<^sub>n\<close>; thus,
 ontologically checked prior arguments \<open>arg\<^sub>1 ... arg\<^sub>n\<^sub>-\<^sub>1\<close> can be ignored during a proof
 process; ontologically, they can be used to assure the traceability of, \<^eg>, semi-formal 
 assumptions throughout their way to formalisation and use in lemmas and proofs. \<close> 
 
-figure*[doc_termAq::figure,relative_width="50",file_src="''figures/doc-mod-term-aq.pdf''"]
+figure*[doc_termAq::figure,relative_width="35",file_src="''figures/doc-mod-term-aq.pdf''"]
                       \<open>Term-Antiquotations Referencing to Annotated Elements\<close>
 text\<open>As shown in @{figure \<open>doc_termAq\<close>}, this feature of  \<^isadof> substantially increases
 the expressibility of links between the formal and the informal in \<^dof> documents.\<close>
@@ -541,14 +525,13 @@ Isabelle/Isar  \<^theory_text>\<open>theorem\<close>-command will in contrast to
 
 Note that the \<^theory_text>\<open>declare_reference*\<close> command will appear in the \<^LaTeX> generated from this 
 document fragment. In order to avoid this, one has to enclose this command into the 
-document comments :\<close>
+document comments : \<open>(*<*) ... (*>*)\<close>.\<close>
-text\<open>\<^center>\<open>\<open>(*<*) ... (*>*)\<close>\<close>\<close>
 
 
 section*[tech_onto::example]\<open>Writing Technical Reports in \<^boxed_theory_text>\<open>technical_report\<close>\<close>  
 text\<open>While it is perfectly possible to write documents in the
-\<^verbatim>\<open>technical_report\<close> ontology in freeform-style (the present manual is mostly an
+\<^verbatim>\<open>technical_report\<close> ontology in freeform-style (this manual is mostly such an
-example for this category), we will briefly explain here the tight-checking-style in which
+example), we will briefly explain here the tight-checking-style in which
 most Isabelle reference manuals themselves are written. 
 
 The idea has already been put forward by Isabelle itself; besides the general infrastructure on 
@@ -601,9 +584,8 @@ text\<open>They are text-contexts equivalents to the \<^theory_text>\<open>term*
      for term-contexts introduced in @{technical (unchecked) \<open>subsec:onto-term-ctxt\<close>}\<close>
 
 subsection\<open>A Technical Report with Tight Checking\<close>
-text\<open>An example of tight checking is a small programming manual developed by the
+text\<open>An example of tight checking is a small programming manual to document programming trick 
-second author in order to document programming trick discoveries while implementing in Isabelle.
+discoveries while implementing in Isabelle. While not necessarily a meeting standards of a scientific text, it appears to us that this information
-While not necessarily a meeting standards of a scientific text, it appears to us that this information
 is often missing in the Isabelle community. 
 
 So, if this text addresses only a very limited audience and will never be famous for its style,
@@ -613,13 +595,13 @@ So its value is that readers can just reuse some of these snippets and adapt the
 purposes.
 \<close>
 
-figure*[strict_SS::figure, relative_width="95", file_src="''figures/MyCommentedIsabelle.png''"] 
+figure*[strict_em::figure, relative_width="95", file_src="''figures/MyCommentedIsabelle.png''"] 
 \<open>A table with a number of SML functions, together with their type.\<close>
 
 text\<open>
-\<open>TR_MyCommentedIsabelle\<close> is written according to the \<^verbatim>\<open>technical_report\<close> ontology in
+This manual  is written according to the \<^verbatim>\<open>technical_report\<close> ontology in
 \<^theory>\<open>Isabelle_DOF.technical_report\<close>.
-\<^figure>\<open>strict_SS\<close> shows a snippet from this integrated source and gives an idea why 
+\<^figure>\<open>strict_em\<close> shows a snippet from this integrated source and gives an idea why 
 its tight-checking allows for keeping track of underlying Isabelle changes:
 Any reference to an SML operation in some library module is type-checked, and the displayed
 SML-type really corresponds to the type of the operations in the underlying SML environment.
@@ -647,8 +629,7 @@ text\<open> This is *\<open>emphasized\<close> and this is a
         citation @{cite "brucker.ea:isabelle-ontologies:2018"}.\<close>
 \<close>}
 The list of standard Isabelle document antiquotations, as well as their options and styles,
-can be found in the Isabelle reference manual @{cite "wenzel:isabelle-isar:2020"}, also be found
+can be found in the Isabelle reference manual @{cite "wenzel:isabelle-isar:2020"}, 
-under \<^url>\<open>https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2022/doc/isar-ref.pdf\<close>, 
 section 4.2.
 
 In practice,  \<^isadof> documents with ambitious layout will contain a certain number of
@@ -657,7 +638,7 @@ not possible. As far as possible, raw \<^LaTeX> should be restricted to the defi
 of ontologies and  macros (see @{docitem (unchecked) \<open>isadof_ontologies\<close>}). If raw 
  \<^LaTeX> commands can not be avoided, it is recommended to use the Isabelle document comment
 \<^latex>\<open>\verb+\+\verb+<^latex>+\<close>\<open>\<open>argument\<close>\<close> to isolate these parts
-(cf. \<^url>\<open>https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2022/doc/isar-ref.pdf\<close>). 
+(cf.  @{cite "wenzel:isabelle-isar:2020"}).
 
 Restricting the use of \<^LaTeX> has two advantages: first, \<^LaTeX> commands can circumvent the 
 consistency checks of \<^isadof> and, hence, only if no \<^LaTeX> commands are used, \<^isadof> can 

Isabelle_DOF/thys/manual/M_04_RefMan.thy

@@ -309,8 +309,8 @@ text\<open>
   Moreover, as usual, special care has to be taken for commands that write into aux-files
   that are included in a following \<^LaTeX>-run. For such complex examples, we refer the interested 
   reader to  the style files provided in the \<^isadof> distribution. In particular 
-  the definitions of the concepts \<^boxed_theory_text>\<open>title*\<close> and \<^boxed_theory_text>\<open>author*\<close> in the 
+  the definitions of the concepts \<^boxed_theory_text>\<open>title*\<close> and \<^boxed_theory_text>\<open>author*\<close> in \<^LaTeX>-style 
-  file \<^file>\<open>../../ontologies/scholarly_paper/DOF-scholarly_paper.sty\<close> show examples of protecting 
+  for the ontology @{theory \<open>Isabelle_DOF.scholarly_paper\<close>} shows examples of protecting 
   special characters in definitions that need to make use of a entries in an aux-file. 
 \<close>
 
@@ -720,11 +720,11 @@ text*[dupl_graphics::float,
 @{fig_content (width=40, height=35, caption="This is a left test") "figures/A.png"
 }\<^hfill>@{fig_content (width=40, height=35, caption="This is a right \<^term>\<open>\<sigma>\<^sub>i + 1\<close> test") "figures/B.png"} 
 \<close>\<close>}\<close>
+
+text\<open>The \<^theory_text>\<open>side_by_side_figure*\<close>-command  \<^bindex>\<open>side\_by\_side\_figure\<close> has been deprecated.\<close>
 (*>*)
 
-text\<open>Note that the \<^theory_text>\<open>side_by_side_figure*\<close>-command  \<^bindex>\<open>side\_by\_side\_figure\<close> used in earlier 
+text\<open>
-versions of \<^dof> thus became obsolete.
-
 \<^verbatim>\<open>COL\<close> finally provides macros that extend the command-language of the DOF core by the following
 abbreviations:
 
@@ -1432,35 +1432,22 @@ text\<open>
   \<^LaTeX>-packages that are (strictly) required by the used \<^LaTeX>-setup. In general, we recommend
   to only add \<^LaTeX>-packages that are always necessary for this particular template, as loading
   packages in the templates minimizes the freedom users have by adapting the \<^path>\<open>preample.tex\<close>.
-  Moreover, you might want to add/modify the template specific configuration 
+  The file name of the new template should start with the prefix \<^path>\<open>root-\<close> and need to be 
-  (\autoref{lst:config-start}-\ref{lst:config-end}). The new template should be stored in 
+  registered using the \<^theory_text>\<open>define_template\<close> command.
-  \<^path>\<open>src/document-templates\<close> and its file name should start with the prefix \<^path>\<open>root-\<close>. After
+  a typical \<^isadof> document template looks as follows: 
-  adding a new template, call the \<^boxed_bash>\<open>install\<close> script (see \<^technical>\<open>infrastructure\<close>).  
-  The common structure of an \<^isadof> document template looks as follows: 
 
 \<^latex>\<open>
 \begin{ltx}[escapechar=ë, numbers=left,numberstyle=\tiny,xleftmargin=5mm]
 \documentclass{article}        % The LaTeX-class of your template ë\label{lst:dc}ë  
-%% The following part is (mostly) required by Isabelle/DOF, do not modify
+\usepackage{DOF-core}
-\usepackage[T1]{fontenc}       % Font encoding
+\usepackage{subcaption}
-\usepackage[utf8]{inputenc}    % UTF8 support
-\usepackage{xcolor}
-\usepackage{isabelle,isabellesym,amssymb} % Required (by Isabelle)
-\usepackage{amsmath}           % Used by some ontologies  
-\bibliographystyle{abbrv}
-\input{dof-common} % setup shared between all Isabelle/DOF templates
-\usepackage{graphicx}          % Required for images. 
-\usepackage[caption]{subfig}
 \usepackage[size=footnotesize]{caption}
-\usepackage{hyperref}          % Required by Isabelle/DOF
+\usepackage{hyperref}
-
-%% Begin of template specific configuration ë\label{lst:config-start}ë
-\urlstyle{rm}
-\isabellestyle{it}     ë\label{lst:config-end}ë
 
 %% Main document, do not modify
 \begin{document}
-\maketitle\input{session}
+\maketitle
+\IfFileExists{dof_session.tex}{\input{dof_session}}{\input{session}}
 \IfFileExists{root.bib}{\bibliography{root}}{}
 \end{document}
 \end{ltx}\<close>
@@ -1607,9 +1594,6 @@ text\<open>
 }
 \end{ltx}\<close>
 
-  For a real-world example testing for multiple classes, see 
-  \<^file>\<open>../../ontologies/scholarly_paper/DOF-scholarly_paper.sty\<close>:
-
   We encourage this clear and machine-checkable enforcement of restrictions while, at the same
   time, we also encourage to provide a package option to overwrite them. The latter allows 
   inherited ontologies to overwrite these restrictions and, therefore, to provide also support

Isabelle_DOF/thys/manual/M_05_Implementation.thy

@@ -146,7 +146,8 @@ text\<open>
 \<open>val _ = Theory.setup
          (docitem_antiquotation  @{binding "docitem"}  DOF_core.default_cid #>
             
-            ML_Antiquotation.inline @{binding "docitem_value"} ML_antiquotation_docitem_value)\<close>}
+        ML_Antiquotation.inline @{binding "docitem_value"} 
+              ML_antiquotation_docitem_value)\<close>}
   the text antiquotation \<^boxed_sml>\<open>docitem\<close> is declared and bounded to a parser for the argument 
   syntax and the overall semantics. This code defines a generic antiquotation to be used in text 
   elements such as