polishing

examples/scholarly_paper/2021-ITP-PMTI/paper.thy

@@ -119,7 +119,7 @@ text*[introtext::introduction]\<open> \<^vs>\<open>-0.2cm\<close>
 The linking of \<^emph>\<open>formal\<close> and \<^emph>\<open>informal\<close> information is perhaps the most pervasive challenge 
 in the digitization of knowledge and its propagation. Unsurprisingly, this problem reappears 
 in the libraries with formalized mathematics and engineering such as the Isabelle Archive of 
-Formal Proofs @{cite "AFP-ref22"}, which passed the impressive numbers of 650 articles, 
+Formal Proofs @{cite "AFP-ref22"} (AFP), which passed the impressive numbers of 650 articles, 
 written by 420 authors at the beginning of 2022. Together with the AFP, there is also a growing 
 body on articles concerned with formal software engineering such as standardized language 
 definitions (e.g., @{cite "CakeML-AFP" and "brucker.ea:featherweight:2014"}), 
@@ -143,7 +143,7 @@ definitions and proofs remains largely open.
 The central role in technologies adressing the \<^emph>\<open>knowledge\<close> problem
 is played by \<^emph>\<open>document ontologies\<close>, \<^ie>, a machine-readable form
 of meta-data attached to document-elements as well as their document discourse. In order 
-to make these techniques applicable to \<^emph>\<open>formal theory development\<close> , 
+to make these techniques applicable to \<^emph>\<open>formal theory development\<close>,
 the following is needed: \<^vs>\<open>0.2cm\<close>
 
 \<^item> a general mechanism to define and develop \<^emph>\<open>domain-specific\<close> ontologies,
@@ -343,9 +343,7 @@ text\<open>\<^vs>\<open>-0.2cm\<close> The types of attributes are \<^hol>-types
           is_concerned::"role set"        (* \<comment> \<open>roles working with this req.\<close> *) \<close>}
   This ODL class definition maybe part of one or more Isabelle theory-files capturing the entire
   ontology definition. Isabelle's session management allows for pre-compiling them before being 
-  imported in the actual target documentation required to be compliant to this ontology. 
-
-%\vspace{-0.7cm}\<close>
+  imported in the actual target document. \<close>
 
 side_by_side_figure*["text-elements"::side_by_side_figure,anchor="''fig-Req-Def-ex''",
                       caption="''A Text-Element as Requirement.''",relative_width="48",
@@ -353,13 +351,11 @@ side_by_side_figure*["text-elements"::side_by_side_figure,anchor="''fig-Req-Def-
                       caption2="''Referencing a Requirement.''",relative_width2="48",
                       src2="''figures/Req-Appl-ex''"]\<open>Referencing a Requirement. \<close>
 
-text\<open>\autoref{text-elements} shows an ontological annotation of a requirement and the referencing
-  via an antiquotation \<^theory_text>\<open>requirement \<open>req1\<close>\<close> generated by \<^dof> from the above 
+text\<open>@{figure "text-elements"} shows an ontological annotation of a requirement and its referencing
+  via an antiquotation \<^theory_text>\<open>requirement \<open>req1\<close>\<close>; the latter is generated from the above 
   class definition. Undefined or ill-typed references were rejected, the high-lighting displays 
-  the hyperlinking which is activated on a click. Revising the actual definition of \<open>requirement\<close>, 
-  it suffices to click on its keyword: the IDE will display the class-definition and its surrounding 
-  documentation in the ontology.\<close>
-
+  the hyperlinking which is activated on a click. The class-definition of \<open>requirement\<close> and its 
+  documentation is also revisited via one activation click.\<close>
 (*
 
 text\<open>\<^dof>'s generated antiquotations are part of a general mechanism of  
@@ -396,24 +392,20 @@ record T =
 
 term "\<lparr>x = a,y = b\<rparr>"
 (*>*)
+text\<open>\<^vs>\<open>-0.2cm\<close> \<^noindent> \<^isabelle> supports records at the level of terms and 
+types. The notation for terms and types is as follows: \<^vs>\<open>-0.2cm\<close>
+\<^item> record terms \<^term>\<open>\<lparr>x = a,y = b\<rparr>\<close> and corresponding record types \<open>\<lparr>x::A, y::B\<rparr>\<close>,
+\<^item> the resulting selectors are written \<^term>\<open>x(r::T)\<close>, \<^term>\<open>y(r::T)\<close>.\<close>
 
-text\<open>
-\<^isabelle> supports records at the level of terms and 
-types. The notation for terms and types is as follows:
-\<^item> record terms \<^term>\<open>\<lparr>x = a,y = b\<rparr>\<close>; record types \<open>\<lparr>x::A, y::B\<rparr>\<close>,
-\<^item> selectors are written \<^term>\<open>x(R::T)\<close>, \<^term>\<open>y(R::T)\<close>.
-\<close>
-
-text\<open>  \<^noindent> In fact, \<^verbatim>\<open>onto_class\<close>es and the logically equivalent  \<^verbatim>\<open>doc_class\<close>es were
-represented by \<^emph>\<open>extensible\<close> record types and instances thereof by HOL terms. 
+text\<open> \<^noindent> In fact, \<^verbatim>\<open>onto_class\<close>es and the logically equivalent  \<^verbatim>\<open>doc_class\<close>es were
+represented by \<^emph>\<open>extensible\<close> record types and instances thereof by HOL terms 
+(see @{cite"brucker.ea:isabelledof:2019"} for details.).  
 Invariants of an \<^verbatim>\<open>onto_class\<close> are just predicates over extensible record
-types and can therefore be applied to a subclass; Details can be found in @{cite"brucker.ea:isabelledof:2019"}.  
-\<close>
-
+types and were applied to subclasses. \<close>
 
 subsection\<open>Term-Evaluations in Isabelle\<close>
 text\<open>Besides the powerful, but relatively slow Isabelle rewriting-based proof method,
- there are  two other techniques for term evaluation:
+ there are  two other techniques for term evaluation: \<^vs>\<open>-0.2cm\<close>
 \<^item> evaluation via reflection @{cite "HaftmannN10"} (\<^theory_text>\<open>eval\<close>), and
 \<^item> normalization by evaluation @{cite "AehligHN12"} (\<^theory_text>\<open>nbe\<close>).\<close>