From a6aca1407e018e7bb7be158604892a8f48a3ac20 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Wed, 19 Apr 2023 21:50:43 +0200 Subject: [PATCH] added sec on term atq, restructuring --- Isabelle_DOF/thys/manual/M_03_GuidedTour.thy | 41 +++++++++----------- 1 file changed, 18 insertions(+), 23 deletions(-) diff --git a/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy b/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy index 20625a8..2a1bb53 100644 --- a/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy +++ b/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy @@ -65,7 +65,6 @@ text\ managers. On a modern Debian system or a Debian derivative (\<^eg>, Ubuntu), the following command should install all required \<^LaTeX> packages: @{boxed_bash [display]\ë\prompt{}ë sudo aptitude install texlive-full\} -\<^dof> \ subsubsection*[isadof::technical]\Installing \<^isadof>\ @@ -216,34 +215,31 @@ text\At times, this causes idiosyncrasies like the ones cited in the follo \ section*[scholar_onto::example]\Writing Academic Publications in \<^boxed_theory_text>\scholarly_paper\\ -subsection\Writing Academic Papers\ +subsection\A Selection of major Examples\ text\ The ontology \<^verbatim>\scholarly_paper\ \<^index>\ontology!scholarly\_paper\ is an ontology modeling academic/scientific papers, with a slight bias towards texts in the domain of mathematics and engineering. We explain first the principles of its underlying ontology, and then we present two ``real'' examples from our own publication practice. -\ -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 are ontologically tracked. However, wrt. - 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 - refrain from integrating references to formal content in order to demonstrate that \<^isadof> is not - a framework from Isabelle users to Isabelle users only, but people just avoiding as much as - possible \<^LaTeX> notation. + \<^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 are ontologically tracked. However, wrt. + 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 + refrain from integrating references to formal content in order to demonstrate that \<^isadof> is not + a framework from Isabelle users to Isabelle users only, but people just avoiding as much as + possible \<^LaTeX> notation. The \<^isadof> distribution contains both examples using the ontology \<^verbatim>\scholarly_paper\ in the directory \<^nolinkurl>\examples/scholarly_paper/2018-cicm-isabelle_dof-applications/\ or \<^nolinkurl>\examples/scholarly_paper/2020-iFM-CSP\. You can inspect/edit the example in Isabelle's IDE, by either - \<^item> starting Isabelle/jEdit using your graphical user interface (\<^eg>, by clicking on the - Isabelle-Icon provided by the Isabelle installation) and loading the file - \<^nolinkurl>\examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy"\ - \<^item> starting Isabelle/jEdit from the command line by, \<^eg>, calling: + \<^item> starting Isabelle/jEdit using your graphical user interface (\<^eg>, by clicking on the + Isabelle-Icon provided by the Isabelle installation) and loading the file + \<^nolinkurl>\examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy"\ + \<^item> starting Isabelle/jEdit from the command line by, \<^eg>, calling: @{boxed_bash [display]\ë\prompt{\isadofdirn}ë isabelle jedit -d . examples/scholarly_paper/2020-iFM-CSP/paper.thy \} @@ -505,10 +501,9 @@ figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood- text\ An ontological reference application in @{figure "figDogfoodVIlinkappl"}: the ontology-dependant antiquotation \<^boxed_theory_text>\@{example \ex1\}\ refers to the corresponding -text-element \<^boxed_theory_text>\ex1\. -Hovering allows for inspection, clicking for jumping to the definition. -If the link does not exist or has a non-compatible type, the text is not validated, \<^ie>, -Isabelle/jEdit will respond with an error.\ +text-element \<^boxed_theory_text>\ex1\. Hovering allows for inspection, clicking for jumping to the +definition. If the link does not exist or has a non-compatible type, the text is not validated, + \<^ie>, Isabelle/jEdit will respond with an error.\ text\We advise users to experiment with different notation variants. Note, further, that the Isabelle \<^latex>\@\{cite ...\}\-text-anti-quotation makes its checking @@ -522,7 +517,7 @@ subsection*["using-term-aq"::technical, main_author = "Some @{author ''bu''}"] text\The present version of \<^isadof> is the first version that supports the novel feature of \<^dof>-generated term-antiquotations\<^bindex>\term-antiquotations\, \<^ie>, antiquotations embedded in HOL-\\\-terms possessing arguments that were validated in the ontological context. -These HOL-\\\-terms may occur in definitions, lemmas, or in values to define attributes +These \\\-terms may occur in definitions, lemmas, or in values to define attributes in class instances. They have the format:\ text\\<^center>\\@{name arg\<^sub>1 ... arg\<^sub>n\<^sub>-\<^sub>1} arg\<^sub>n\\\