diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index eea9246..88b3327 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -526,12 +526,11 @@ text\The \<^verbatim>\scholarly_paper\ ontology extends \<^ve .3 scholarly\_paper.annex{...}. .3 scholarly\_paper.example{...}. .3 scholarly\_paper.technical{Freeform Class for Technical Content}. -.4 ... .4 scholarly\_paper.math\_content{...}. -.5 scholarly\_paper.definition{Freeform Definition}. -.5 scholarly\_paper.lemma{Freeform Lemma}. -.5 scholarly\_paper.theorem{...}. -.5 scholarly\_paper.corollary{...}. +.5 scholarly\_paper.definition{Freeform}. +.5 scholarly\_paper.lemma{Freeform}. +.5 scholarly\_paper.theorem{Freeform}. +.5 scholarly\_paper.corollary{Freeform}. .5 scholarly\_paper.math\_example{...}. .5 scholarly\_paper.math\_semiformal{...}. .4 scholarly\_paper.tech\_example{...}. @@ -541,6 +540,7 @@ text\The \<^verbatim>\scholarly_paper\ ontology extends \<^ve .5 scholarly\_paper.data{...}. .5 scholarly\_paper.evaluation{...}. .5 scholarly\_paper.experiment{...}. +.4 ... .1 ... .1 scholarly\_paper.article{The Paper Monitor}. .1 \ldots. @@ -549,12 +549,21 @@ text\The \<^verbatim>\scholarly_paper\ ontology extends \<^ve \end{center} \ -text\They were alltogether also supported +text\Some of these concepts were supported as command-abbreviations leading to the extension +of the \<^isadof> language: +\<^item> \derived_text_elements \ : +\<^rail>\ + ( ( @@{command "author*"} + | @@{command "abstract*"} + | @@{command "Definition*"} | @@{command "Lemma*"} | @@{command "Theorem*"} + ) + \ + '[' meta_args ']' '\' text '\' + ) + \ \ - - subsubsection*["text-elements-expls"::technical]\Examples\ text\