diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index 9b7115a..d1fa7f6 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -880,7 +880,7 @@ class defined as a list of products characterised by their mass value. This class contains a local \<^theory_text>\invariant c2\ to guarantee that its own mass value equals the sum of all the masses of the products composing the object. For the sake of the argument, we use the reference ontology (considered as a standard) -described in this listing : +described in this listing: %\begin{figure} @{boxed_theory_text [display] \definition sum where "sum S = (fold (+) S 0)" @@ -923,7 +923,7 @@ and the reference ontology using morphism functions (or mapping rules as in ATL or EXPRESS-X language~@{cite "BGPP95"}). These rules are applied to define the relationship between one class of the local ontology to one or several other class(es) described in the reference ontology. In our case, we have define two morphises, \<^const>\Product_to_Component_morphism\ -and \<^const>\Computer_Hardware_to_Hardware_morphism\, detailed in the following listing : +and \<^const>\Computer_Hardware_to_Hardware_morphism\, detailed in the following listing: %\begin{figure} @{boxed_theory_text [display]