From d655effcf8ff9cd7e8bf727e6a48c9fb644d41d2 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Tue, 22 Sep 2020 16:47:05 +0200 Subject: [PATCH] pushup. --- .../Isabelle_DOF-Manual/00_Frontmatter.thy | 6 ------ .../Isabelle_DOF-Manual/document/preamble.tex | 3 --- .../scholarly_paper/DOF-scholarly_paper.sty | 7 +++++++ src/ontologies/scholarly_paper/scholarly_paper.thy | 12 +++++++++++- 4 files changed, 18 insertions(+), 10 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy index 88f99b1..fdf180d 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy @@ -21,12 +21,6 @@ text\Some internal setup, introducing document specific abbreviations and 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>\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" #> DOF_lib.define_shortcut \<^binding>\BibTeX\ "\\BibTeX{}" #> DOF_lib.define_shortcut \<^binding>\LaTeX\ "\\LaTeX{}" diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex index 4f00967..4495160 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex +++ b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex @@ -29,9 +29,6 @@ %\makeindex %\AtEndDocument{\printindex} -\newcommand{\ie}{i.e.} -\newcommand{\eg}{e.g.} -\newcommand{\etc}{etc} \newcommand{\dof}{DOF\xspace} \newcommand{\path}[1]{\texttt{\nolinkurl{#1}}} diff --git a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty index 3bfd61a..be35093 100755 --- a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty +++ b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty @@ -477,3 +477,10 @@ }% \end{isamarkuptext}% } + + +%% Miscellaneous +\newcommand{\ie}{i.e.} +\newcommand{\eg}{e.g.} +\newcommand{\etc}{etc} + diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index acd6c51..ce594d4 100755 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -418,10 +418,20 @@ fun check_group a = map (check_group_elem (check_level_hd (hd a))) (tl a) ; *) \ -section\Miscelleous: Layout Trimming Commands\ +section\Miscelleous\ +subsection\Layout Trimming Commands\ setup\ DOF_lib.define_macro \<^binding>\hs\ "\\hspace{" "}" (K(K())) \ setup\ DOF_lib.define_macro \<^binding>\vs\ "\\vspace{" "}" (K(K())) \ +subsection\Common Abbreviations\ +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>\etc\ "\\etc"\ + (* Latin: „id est“ meaning „that is to say“. *) + (* this is an alternative style for macro definitions equivalent to setup ... setup ...*) + + end