diff --git a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy index 42848a24..b35a95df 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy @@ -140,7 +140,8 @@ abstract*[abs, keywordlist="[\Ontology\, \Ontological Modelin the link between formal and informal content in documents in a machine checked way. These links can connect both text elements as well as formal modelling elements such as terms, definitions, code and logical formulas, - alltogether *\integrated\ in a state-of-the-art interactive theorem prover. + alltogether \<^emph>\integrated\ in a state-of-the-art interactive theorem prover. + \ (*<*) diff --git a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy index 79f5a19a..7acdcf5e 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy @@ -91,7 +91,7 @@ text\ by simp\} \<^item> a green background for examples of generated document fragments (\<^ie>, PDF output): @{boxed_pdf [display] \The axiom refl\} - \<^item> a red background for For (S)ML-code: + \<^item> a red background for (S)ML-code: @{boxed_sml [display] \fun id x = x\} \<^item> a yellow background for \LaTeX-code: @{boxed_latex [display] \\newcommand{\refl}{$x = x$}\} diff --git a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy index 9ef95920..53b5d021 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy @@ -153,7 +153,7 @@ text\ "wenzel:system:2014" and "barras.ea:pervasive:2013" and "faithfull.ea:coqoon:2018"} which in many features over-accomplishes the required features of \<^dof>. For example, current Isabelle versions offer cascade-syntaxes (different syntaxes and even parser-technologies which can be - nested along the \\...\\ barriers, while \<^dof> actually only requires a two-level syntax model. + nested along the \\...\\ barriers), while \<^dof> actually only requires a two-level syntax model. \ (* end experiment *) diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index 6805a418..fd2e4ced 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -267,7 +267,7 @@ users are: files required by the document generation (\<^eg>, images, bibliography database using \<^BibTeX>, local \<^LaTeX>-styles) need to be registered in this file. For details of Isabelle's build system, please consult the Isabelle System Manual~@{cite "wenzel:system-manual:2020"}. -\<^item> The file \<^boxed_bash>\praemble.tex\\<^index>\praemble.tex\, which allows users to add additional +\<^item> The file \<^boxed_bash>\preamble.tex\\<^index>\preamble.tex\, which allows users to add additional \<^LaTeX>-packages or to add/modify \<^LaTeX>-commands. \ @@ -284,7 +284,7 @@ text\ \<^enum> The iFM 2020 paper~@{cite "taha.ea:philosophers:2020"} is 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 is ontologically tracked. However, wrt. - to the possible linking between the underlying formal theory and this mathematical presentation, + 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, deliberately not exploiting \<^isadof> 's full potential with this regard. \<^enum> In the CICM 2018 paper~@{cite "brucker.ea:isabelle-ontologies:2018"}, we deliberately @@ -346,7 +346,7 @@ context of this document; this is a decisive feature of \<^isadof> that conventi languages lack.\ text\We continue by the introduction of a main class: the text-element \text_section\ (in contrast -to \figure\ or \table\ or similar. Note that +to \figure\ or \table\ or similar). Note that the \main_author\ is typed with the class \author\, a HOL type that is automatically derived from the document class definition \author\ shown above. It is used to express which author currently ``owns'' this \text_section\, an information that can give rise to presentational or even @@ -460,7 +460,7 @@ later is shown in \<^figure>\fig01\ in its presentation as the inte Note that the use in the ontology-generated antiquotation \<^theory_text>\@{definition X4}\ is type-checked; referencing \<^verbatim>\X4\ as \<^theory_text>\theorem\ would be a type-error and be reported directly -by \<^isadof> in Isabelle/jEdit. Note further, that if referenced correctly wrt. to the sub-typing +by \<^isadof> in Isabelle/jEdit. Note further, that if referenced correctly wrt. the sub-typing hierarchy makes \<^verbatim>\X4\ \<^emph>\navigable\ in Isabelle/jedit; a click will cause the IDE to present the defining occurrence of this text-element in the integrated source. @@ -528,7 +528,7 @@ doc_class related_work = conclusion + \} *) text\ In the following, we present some other text-elements provided by the Common Ontology Library -in @{theory "Isabelle_DOF.Isa_COL"}. it provides a document class for figures: +in @{theory "Isabelle_DOF.Isa_COL"}. It provides a document class for figures: @{boxed_theory_text [display]\ datatype placement = h | t | b | ht | hb @@ -651,7 +651,7 @@ text\ which is usually a collaborative effort. As in many other cases, formal certification documents come with an own terminology and pragmatics - of what has to be demonstrated and where, and how the trace-ability of requirements through + of what has to be demonstrated and where, and how the traceability of requirements through design-models over code to system environment assumptions has to be assured. In the sequel, we present a simplified version of an ontological model used in a @@ -675,7 +675,7 @@ doc_class assumption = requirement + Such ontologies can be enriched by larger explanations and examples, which may help the team of engineers substantially when developing the central document for a certification, -like an explication what is precisely the difference between an \<^emph>\hypothesis\ and an +like an explication of what is precisely the difference between an \<^emph>\hypothesis\ and an \<^emph>\assumption\ in the context of the evaluation standard. Since the PIDE makes for each document class its definition available by a simple mouse-click, this kind on meta-knowledge can be made far more accessible during the document evolution. @@ -683,23 +683,23 @@ can be made far more accessible during the document evolution. For example, the term of category \<^emph>\assumption\ is used for domain-specific assumptions. It has formal, semi-formal and informal sub-categories. They have to be tracked and discharged by appropriate validation procedures within a -certification process, by it by test or proof. It is different from a hypothesis, which is +certification process, be it by test or proof. It is different from a hypothesis, which is globally assumed and accepted. In the sequel, the category \<^emph>\exported constraint\ (or \<^emph>\ec\ for short) is used for formal assumptions, that arise during the analysis, design or implementation and have to be tracked till the final evaluation target, and discharged by appropriate validation procedures -within the certification process, by it by test or proof. A particular class of interest -is the category \<^emph>\safety related application condition\ (or \<^emph>\srac\ +within the certification process, be it by test or proof. A particular class of interest +is the category \<^emph>\safety related application condition\ (or \<^emph>\SRAC\ for short) which is used for \<^emph>\ec\'s that establish safety properties -of the evaluation target. Their track-ability throughout the certification +of the evaluation target. Their traceability throughout the certification is therefore particularly critical. This is naturally modeled as follows: @{boxed_theory_text [display]\ doc_class ec = assumption + assumption_kind :: ass_kind <= (*default *) formal -doc_class srac = ec + +doc_class SRAC = ec + assumption_kind :: ass_kind <= (*default *) formal \} @@ -725,7 +725,7 @@ subsection*[ontopide::technical]\Editing Support for CENELEC 50128\ figure*[figfig3::figure,relative_width="95",src="''figures/antiquotations-PIDE''"] \ Standard antiquotations referring to theory elements.\ text\ The corresponding view in @{docitem \figfig3\} shows core part of a document -conformimg to the CENELEC 50128 ontology. The first sample shows standard Isabelle antiquotations +conforming to the CENELEC 50128 ontology. The first sample shows standard Isabelle antiquotations @{cite "wenzel:isabelle-isar:2020"} into formal entities of a theory. This way, the informal parts of a document get ``formal content'' and become more robust under change.\ @@ -882,14 +882,14 @@ underlying logical context, which turns the arguments into \<^emph>\formal source, in contrast to the free-form antiquotations which basically influence the presentation. We still mention a few of these document antiquotations here: -\<^item> \<^theory_text>\@{thm \refl\}\ ou \<^theory_text>\@{thm [display] \refl\}\ check that \<^theory_text>\refl\ is indeed a reference +\<^item> \<^theory_text>\@{thm \refl\}\ or \<^theory_text>\@{thm [display] \refl\}\ check that \<^theory_text>\refl\ is indeed a reference to a theorem; the additional "style" argument changes the presentation by printing the formula into the output instead of the reference itself, \<^item> \<^theory_text>\@{lemma \prop\ } by \method\\ allows to derive \prop\ on the fly, thus garantee that it is a corrollary of the current context, \<^item> \<^theory_text>\@{term \term\ }\ parses and type-checks \term\, \<^item> \<^theory_text>\@{value \term\ }\ performs the evaluation of \term\, -\<^item> \<^theory_text>\@{ML \ml-term\ }\ pa,rses and type-checks \ml-term\, +\<^item> \<^theory_text>\@{ML \ml-term\ }\ parses and type-checks \ml-term\, \<^item> \<^theory_text>\@{ML_file \ml-file\ }\ parses the path for \ml-file\ and verifies its existance in the (Isabelle-virtual) file-system, \<^item> ... @@ -900,9 +900,9 @@ Isabelle. This may be over-precise and a burden to readers not familiar with Isa motivate authors to choose the aforementioned freeform-style. \ -subsection\A \<^verbatim>\technical_report\ in tight-checking-style: \MyCommentedIsabelle\ - Programming Manual \ +subsection\A \<^verbatim>\technical_report\ in tight-checking-style: \TR_MyCommentedIsabelle\ - Programming Manual \ -text\An example of tight checking is a small programming programming manual developed by the +text\An example of tight checking is a small programming manual developed by the second author in order to document programming trick discoveries while implementing in Isabelle. While not necessarily a meeting standards of a scientific text, it appears to us that this information is often missing in the Isabelle community. @@ -934,9 +934,9 @@ figure*[strict_SS::figure, relative_width="95", src="''figures/MyCommentedIsabel \A table with a number of SML functions, together with their type.\ text\ -\MyCommentedIsabelle\ is written according to the @{theory "Isabelle_DOF.technical_report"} -ontology. \<^figure>\strict_SS\ shows a snippet from this integrated source gives an idea why -it tight-checking allows for keeping track of underlying Isabelle changes: +\TR_MyCommentedIsabelle\ is written according to the @{theory "Isabelle_DOF.technical_report"} +ontology. \<^figure>\strict_SS\ 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. In the pdf output, these text-fragments were displayed verbatim. @@ -976,7 +976,7 @@ document generation (\<^eg>, HTML) which, naturally, are only available to docum too complex native \<^LaTeX>-commands. Similarly, (unchecked) forward references should, if possible, be avoided, as they also might -create dangeling references during the document generation that break the document generation. +create dangling references during the document generation that break the document generation. Finally, we recommend to use the @{command "check_doc_global"} command at the end of your document to check the global reference structure. diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index c089ee5a..6a1ef8c6 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -119,7 +119,7 @@ text\ text\ The \<^isadof> ontology specification language consists basically on a notation for document classes, - where the attributes were typed with HOL-types and can be instantiated by terms HOL-terms, \<^ie>, + where the attributes were typed with HOL-types and can be instantiated by HOL-terms, \<^ie>, the actual parsers and type-checkers of the Isabelle system were reused. This has the particular advantage that \<^isadof> commands can be arbitrarily mixed with Isabelle/HOL commands providing the machinery for type declarations and term specifications such @@ -153,7 +153,7 @@ text\ \<^boxed_theory_text>\_ option\, \<^boxed_theory_text>\_ list\, \<^boxed_theory_text>\_ set\, or products \<^boxed_theory_text>\_ \ _\. As a consequence of the document model, ODL definitions may be arbitrarily intertwined with standard HOL type definitions. - Finally, document class definitions result in themselves in a HOL-types in order to allow \<^emph>\links\ + Finally, document class definitions result in themselves in a HOL-type in order to allow \<^emph>\links\ to and between ontological concepts. \ @@ -167,7 +167,7 @@ text\ in \<^isadof>: \<^item> \name\:\<^index>\name@\name\\ with the syntactic category of \name\'s we refer to alpha-numerical identifiers - (called \short_id\'s in @{cite "wenzel:isabelle-isar:2020"}) and identifiers + (called \short_ident\'s in @{cite "wenzel:isabelle-isar:2020"}) and identifiers in \<^boxed_theory_text>\ ... \ which might contain certain ``quasi-letters'' such as \<^boxed_theory_text>\_\, \<^boxed_theory_text>\-\, \<^boxed_theory_text>\.\ (see~@{cite "wenzel:isabelle-isar:2020"} for details). @@ -230,7 +230,7 @@ A document class\<^bindex>\document class\ can be defined using the \<^item> \attribute_decl\:\<^index>\attribute\_decl@\attribute_decl\\ \<^rail>\ name '::' '"' type '"' default_clause? \ \<^item> \invariant_decl\:\<^index>\invariant\_decl@\invariant_decl\\ - An invariants can be specified as predicate over document classes represented as + Invariants can be specified as predicates over document classes represented as records in HOL. Note that sufficient type information must be provided in order to disambiguate the argument of the \\\-expression. \<^rail>\ 'inv' (name '::')? '"' term '"' \ @@ -254,7 +254,7 @@ text\ \inlineltx|\newisadof[]{}|\<^index>\newisadof@\inlineltx{\newisadof}\\<^index>\document class!PDF\ command for defining a dedicated layout for a document class in \<^LaTeX>. Such a document class-specific \<^LaTeX>-definition can not only provide a specific layout (\<^eg>, a specific - highlighting, printing of certain attributes), it can also generate entries in in the table of + highlighting, printing of certain attributes), it can also generate entries in the table of contents or an index. Overall, the \inlineltx|\newisadof[]{}| command follows the structure of the \<^boxed_theory_text>\doc_class\-command: @@ -339,7 +339,7 @@ layout (such as \<^LaTeX>); these commands have to be wrapped into \<^verbatim>\(*<*) ... (*>*)\ brackets if this is undesired. \ subsection\Ontologic Text-Elements and their Management\ -text\ \<^theory_text>\text*[oid::cid, ...] \\\ \ text \ \\\ \ is the core-command of \<^isadof>: it permits to create +text\ \<^theory_text>\text*[oid::cid, ...] \ \ text \ \ \ is the core-command of \<^isadof>: it permits to create an object of meta-data belonging to the class \<^theory_text>\cid\. This is viewed as the \<^emph>\definition\ of an instance of a document class. This instance object is attached to the text-element and makes it thus "trackable" for \<^isadof>, \<^ie>, it can be referenced via the \<^theory_text>\oid\, its attributes @@ -1039,7 +1039,7 @@ text\ \<^path>\llncs.cls\), which cannot be re-distributed due to copyright restrictions. \ -subsection\Developing Ontologies and their Represenation Mappings\ +subsection\Developing Ontologies and their Representation Mappings\ text\ The document core \<^emph>\may\, but \<^emph>\must\ not use Isabelle definitions or proofs for checking the formal content---this manual is actually an example of a document not containing any proof. @@ -1194,7 +1194,7 @@ text\ subsection\Tips, Tricks, and Known Limitations\ text\ - In this sectin, we sill discuss several tips and tricks for developing + In this section, we will discuss several tips and tricks for developing new or adapting existing document templates or \<^LaTeX>-represenations of ontologies. \