Spell Checking.

Isabelle_DOF/thys/manual/M_00_Frontmatter.thy

@@ -124,7 +124,7 @@ abstract*[abs, keywordlist="[\<open>Ontology\<close>, \<open>Ontological Modelin
     A major application of \<^dof> is the integrated development of
     formal certification documents (\<^eg>, for Common Criteria or CENELEC
     50128) that require consistency across both formal and informal
-    arguments. 
+    arguments.
 
     \<^isadof> is integrated into Isabelle's IDE, which
     allows for smooth ontology development as well as immediate

Isabelle_DOF/thys/manual/M_01_Introduction.thy

@@ -31,7 +31,7 @@ Such ontologies can be used for the scientific discourse within scholarly articl
 libraries, and in the engineering discourse of standardized software certification 
 documents~@{cite "boulanger:cenelec-50128:2015" and "cc:cc-part3:2006"}. All these
 documents contain formal content and have to follow a given structure.  In practice, large groups of developers have to produce a substantial
-set of documents where  consistency is notoriously difficult to maintain. In particular, 
+set of documents where consistency is notoriously difficult to maintain. In particular, 
 certifications are centred around the \<^emph>\<open>traceability\<close> of requirements throughout the entire 
 set of documents. While technical solutions for the traceability problem exist (most notably:
 DOORS~@{cite "ibm:doors:2019"}), they are weak in the treatment of formal entities (such as formulas 
@@ -65,7 +65,7 @@ track and trace links in texts. It is an \<^emph>\<open>environment to write str
 scientific papers---as the present one, which is written in \<^isadof> itself. \<^isadof> is a plugin 
 into the Isabelle/Isar framework in the style of~@{cite "wenzel.ea:building:2007"}. However,
  \<^isadof> will generate from ontologies a theory infrastructure consisting of types, terms, theorems
-and code that allows both interactive checking as well as formal reasoning over meta-data
+and code that allows both interactive checking and formal reasoning over meta-data
 related to annotated documents.\<close>
 
 subsubsection\<open>How to Read This Manual\<close>

Isabelle_DOF/thys/manual/M_02_Background.thy

@@ -118,9 +118,9 @@ text\<open> A simple text-element \<^index>\<open>text-element\<close> may look
 
   @{boxed_theory_text [display]\<open>
 text\<open> This is a simple text.\<close>\<close>}
-... so it is a command \<^theory_text>\<open>text\<close> followed by an argument (here in  \<open>\<open> ... \<close>\<close> parenthesis) which 
-contains characters. While \<^theory_text>\<open>text\<close>- elements play a major role in this manual --- document 
-generation is the main use-case of \<^dof> in its current stage --- it is important to note that there 
+\ldots so it is a command \<^theory_text>\<open>text\<close> followed by an argument (here in  \<open>\<open> ... \<close>\<close> parenthesis) which 
+contains characters. While \<^theory_text>\<open>text\<close>-elements play a major role in this manual---document 
+generation is the main use-case of \<^dof> in its current stage---it is important to note that there 
 are actually three families of ``ontology aware'' document elements with analogous 
 syntax to standard ones. The difference is a bracket with meta-data of the form:
 @{theory_text [display,indent=5, margin=70] 
@@ -130,7 +130,7 @@ ML*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> s
 value*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> some annotated \<lambda>-term \<close>
 \<close>}
 
-Other instances of document elements belonging to these families are, for example, the freeform
+Other instances of document elements belonging to these families are, for example, the free-form
 \<^theory_text>\<open>Definition*\<close> and \<^theory_text>\<open>Lemma*\<close> as well as their formal counterparts \<^theory_text>\<open>definition*\<close> and \<^theory_text>\<open>lemma*\<close>,
 which allow in addition to their standard Isabelle functionality the creation and management of
 ontology-generated meta-data associated to them (cf. -@{text_section (unchecked) "writing_doc"}).
@@ -214,14 +214,14 @@ figure*["fig_dof_ide",relative_width="95",file_src="''figures/cicm2018-combined.
 
 text\<open> 
   We call the present implementation of \<^dof> on the Isabelle platform  \<^isadof> . 
-  @{figure  "fig_dof_ide"} shows  a screen-shot of an introductory paper on 
+  @{figure  "fig_dof_ide"} shows a screenshot of an introductory paper on 
   \<^isadof>~@{cite "brucker.ea:isabelle-ontologies:2018"}: the \<^isadof> PIDE can be seen on the left, 
   while the generated presentation in PDF is shown on the right.
 
   Isabelle provides, beyond the features required for \<^dof>, a lot of additional benefits. 
   Besides UTF8-support for characters used in text-elements, Isabelle offers built-in already a 
   mechanism for user-programmable antiquotations \<^index>\<open>antiquotations\<close> which we use to implement
-  semantic macros  \<^index>\<open>semantic macros\<close> in \<^isadof> (We will actually use these two terms
+  semantic macros \<^index>\<open>semantic macros\<close> in \<^isadof> (We will actually use these two terms
   as synonym in the context of \<^isadof>). Moreover, \<^isadof> allows for the asynchronous 
   evaluation and checking of the document content~@{cite "wenzel:asynchronous:2014" and 
   "wenzel:system:2014" and "barras.ea:pervasive:2013"} and is dynamically extensible. Its PIDE 

Isabelle_DOF/thys/manual/M_03_GuidedTour.thy

@@ -80,9 +80,9 @@ is currently consisting out of three AFP entries:
  \<^LaTeX>.
 \<^item> \<^verbatim>\<open>Isabelle_DOF-Example-II\<close>: This entry contains another example of 
   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 
+  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, with respect to 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.\<close>
 
@@ -177,7 +177,7 @@ There are actually different name categories that form a proper name space, \<^e
 constant symbols and type symbols are distinguished.
 Additionally, \<^isadof> objects also come with a proper name space: classes (and monitors), instances,
 low-level class invariants (SML-defined invariants) all follow the lexical conventions of
-Isabelle. For instance, a class can be referenced outside of its theory using
+Isabelle. For instance, a class can be referenced outside its theory using
 its short-name or its long-name if another class with the same name is defined
 in the current theory.
 Isabelle identifies names already with the shortest suffix that is unique in the global 
@@ -188,7 +188,7 @@ be printed with different prefixes according to their uniqueness.
 
 subsection*[cartouches::example]\<open>Caveat: Lexical Conventions of Cartouches, Strings, Names, ... \<close>
 text\<open>WARNING: The embedding of strings, terms, names \<^etc>, as parts of commands, anti-quotations,
-terms,  \<^etc>, is unfortunately not always so consistent as one might expect, when it comes
+terms, \<^etc>, is unfortunately not always so consistent as one might expect, when it comes
 to variants that should be lexically equivalent in principle. This can be a nuisance for
 users, but is again a consequence that we build on existing technology that has been developed
 over decades. 

Isabelle_DOF/thys/manual/M_05_Proofs_Ontologies.thy

@@ -233,8 +233,6 @@ text\<open>The proof is, in order to quote Tony Hoare, ``as simple as it should
 the lemmas like @{thm concatWith_non_mt} which in itself require inductions, \<^ie>, which are out of
 reach of pure ATP proof-techniques. \<close>
 
-
-
 subsection\<open>Proving the Preservation of Ontological Mappings : A Domain-Ontology Morphism\<close>
 text\<open>The following example is drawn from a domain-specific scenario: For conventional data-models,
 be it represented by UML-class diagrams or SQL-like "tables" or Excel-sheet like presentations
@@ -453,5 +451,4 @@ no_notation Times (infixr "~~" 60)
 no_notation Atom  ("\<lfloor>_\<rfloor>" 65)
 
 end
-(*>*) 
-  
+(*>*) 

Isabelle_DOF/thys/manual/M_06_RefMan.thy

@@ -807,7 +807,7 @@ doc_class text_section = text_element +
 
 Besides attributes of more practical considerations like a \<^const>\<open>fixme_list\<close>, that can be modified
 during the editing process but is only visible in the integrated source but usually ignored in the
-\<^LaTeX>, this class also introduces the possibility to assign an ``ownership" or ``responsibility" of 
+\<^LaTeX>, this class also introduces the possibility to assign an ``ownership'' or ``responsibility'' of 
 a \<^typ>\<open>text_element\<close> to a specific \<^typ>\<open>author\<close>. Note that this is possible since \<^isadof> assigns to each
 document class also a class-type which is declared in the HOL environment.\<close>