diff --git a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy index 2630743d..c5fab07d 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy @@ -23,7 +23,8 @@ setup \DOF_lib.define_shortcut \<^binding>\dof\ "\\dof" setup \DOF_lib.define_shortcut \<^binding>\isadof\ "\\isadof"\ setup \ DOF_lib.define_shortcut \<^binding>\eg\ "\\eg" (* Latin: „exempli gratia“ meaning „for example“. *) - #> DOF_lib.define_shortcut \<^binding>\ie\ "\\ie"\ + #> DOF_lib.define_shortcut \<^binding>\ie\ "\\ie" + #> DOF_lib.define_shortcut \<^binding>\etc\ "\\etc"\ (* Latin: „id est“ meaning „that is to say“. *) (* this is an alternative style for macro definitions equivalent to setup ... setup ...*) setup \ DOF_lib.define_shortcut \<^binding>\TeXLive\"\\TeXLive" diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index cf7d4d08..e93ad0db 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -411,13 +411,45 @@ figure*[fig0B::figure,spawn_columns=False,relative_width="95",src="''figures/hea \ \ldots and as its resulting \<^pdf>-output. \ text\Recall that the standard syntax for a text-element in \<^isadof> is -\<^theory_text>\text*[::,]\ ... text ...\\, but there are a few built-in abbreviations like +\<^theory_text>\text*[::,]\ ... text ...\\, but there are a few built-in abbreviations like \<^theory_text>\title*[,]\ ... text ...\\ that provide special command-level syntax for text-elements. The other text-elements provide the authors and the abstract as specified by their class-id referring to the \<^theory_text>\doc_class\es of \<^verbatim>\scholarly_paper\; we say that these text elements are \<^emph>\instances\ -\<^bindex>\instance\ of the \<^theory_text>\doc_class\es \<^bindex>\doc_class\ of the underlying ontology. \ +\<^bindex>\instance\ of the \<^theory_text>\doc_class\es \<^bindex>\doc\_class\ of the underlying ontology. \ + +text\The paper proceeds by providing instances for introduction, technical sections, examples, \<^etc>. +We would like to concentrate on one --- mathematical paper oriented --- detail in the ontology +\<^verbatim>\scholarly_paper\: +@{theory_text [display] +\doc_class technical = text_section + + . . . + +type_synonym tc = technical (* technical content *) + +datatype math_content_class = "defn" | "axm" | "thm" | "lem" | "cor" | "prop" | ... + +doc_class math_content = tc + + ... + +doc_class "definition" = math_content + + mcc :: "math_content_class" <= "defn" + ... + +doc_class "theorem" = math_content + + mcc :: "math_content_class" <= "thm" + ... +\}\ + +text\The class \<^verbatim>\technical\ regroups a number of text-elements that contain typical +"technical content" in mathematical or engineering papers: code, definitions, theorems, +lemmas, examples. From this class, the more stricter class of @{typ \math_content\} is derived, +which is grouped into @{typ "definition"}s and @{typ "theorem"}s (the details of these +class definitions are omitted here). Note, however, that class identifiers can be abbreviated by +standard \<^theory_text>\type_synonym\s for convenience and enumeration types can be defined by the +standard inductive \<^theory_text>\datatype\ definition mechanism in Isabelle, since any HOL type is admitted +for attibute declarations. Vice-versa, document class definitions imply a corresponding HOL type +definition. \ -text\The paper proceeds by providing instances for introduction, technical sections, examples, TODO\ subsection\Writing Academic Publications II (somewhat outdated)\ text\ In our next example we concentrate on non-text-elements. Focus on Figures... @@ -657,6 +689,7 @@ safety-related condition; however, this happens in a context where general \<^em are listed. \<^isadof>'s checks establish that this is legal in the given ontology. \ +(* section*[math_exam::example]\Writing Exams (math\_exam)\ subsection\The Math Exam Example\ text\ @@ -779,6 +812,7 @@ In our scenario this sample proofs are completely \<^emph>\intern\, students but just additional material for the internal review process of the exam. \ +*) section\Style Guide\ text\ diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/header_CSP_pdf.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/header_CSP_pdf.png new file mode 100644 index 00000000..ef600ab6 Binary files /dev/null and b/examples/technical_report/Isabelle_DOF-Manual/document/figures/header_CSP_pdf.png differ diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/header_CSP_source.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/header_CSP_source.png new file mode 100644 index 00000000..598cd919 Binary files /dev/null and b/examples/technical_report/Isabelle_DOF-Manual/document/figures/header_CSP_source.png differ diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex index cb3fa34a..38908fb4 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex +++ b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex @@ -31,6 +31,7 @@ \newcommand{\ie}{i.e.} \newcommand{\eg}{e.g.} +\newcommand{\etc}{etc} \newcommand{\path}[1]{\texttt{\nolinkurl{#1}}} \title{} \author{<AUTHOR>}