diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy index e3565a4..a99c644 100755 --- a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy +++ b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy @@ -21,6 +21,7 @@ declare[[strict_monitor_checking=false]] setup \ DOF_lib.define_shortcut \<^binding>\isadof\ "\\isadof" #> DOF_lib.define_shortcut \<^binding>\LaTeX\ "\\LaTeX{}" + #> DOF_lib.define_shortcut \<^binding>\dots\ "\\ldots" #> DOF_lib.define_shortcut \<^binding>\isabelle\ "Isabelle/HOL"\ (*>*) @@ -161,8 +162,8 @@ automated proof procedures as well as specific support for higher specification were built. \ text\ We would like to detail the documentation generation of the architecture, -which is based on literate specification commands such as \inlineisar+section+ \ldots, -\inlineisar+subsection+ \ldots, \inlineisar+text+ \ldots, etc. +which is based on literate specification commands such as \inlineisar+section+ \<^dots>, +\inlineisar+subsection+ \<^dots>, \inlineisar+text+ \<^dots>, etc. Thus, a user can add a simple text: \begin{isar} text\This is a description.\ @@ -311,7 +312,7 @@ The translation of its content to, \<^eg>, Springer's \<^LaTeX> setup for the Le Science Series, as required by many scientific conferences, is mostly straight-forward. \ figure*[fig1::figure,spawn_columns=False,relative_width="95",src="''figures/Dogfood-Intro''"] - \ Ouroboros I: This paper from inside \ldots \ + \ Ouroboros I: This paper from inside \<^dots> \ text\ @{figure \fig1\} shows the corresponding view in the Isabelle/PIDE of thqqe present paper. Note that the text uses \<^isadof>'s own text-commands containing the meta-information provided by @@ -400,7 +401,7 @@ and semantic convenience. Choosing the mathematical reals, \<^eg>, would have th attribute evaluation could be substantially more complicated.\ figure*[fig_figures::figure,spawn_columns=False,relative_width="85",src="''figures/Dogfood-figures''"] - \ Ouroboros II: figures \ldots \ + \ Ouroboros II: figures \<^dots> \ text\ The document class \inlineisar+figure+ --- supported by the \<^isadof> text command \inlineisar+figure*+ --- makes it possible to express the pictures and diagrams in this paper @@ -529,7 +530,7 @@ derivation---as part of an algebra exercise, for example---which is submitted to electronically. \ figure*[fig_qcm::figure,spawn_columns=False, relative_width="90",src="''figures/InteractiveMathSheet''"] - \ A Generated QCM Fragment \ldots \ + \ A Generated QCM Fragment \<^dots> \ subsection*[cenelec_onto::example]\ The Certification Scenario following CENELEC \ text\ Documents to be provided in formal certifications (such as CENELEC @@ -653,7 +654,7 @@ device. This condition can not be established inside the formal theory but has t checked by system integration tests.\ figure*[figfig5::figure, relative_width="80", src="''figures/srac-definition''"] - \ Defining a SRAC reference \ldots \ + \ Defining a SRAC reference \<^dots> \ figure*[figfig7::figure, relative_width="80", src="''figures/srac-as-es-application''"] \ Using a SRAC as EC document reference. \