pushup, stiluebungen.

examples/scholarly_paper/2020-iFM-CSP/paper.thy

@@ -15,7 +15,6 @@ setup \<open>   DOF_lib.define_shortcut \<^binding>\<open>eg\<close>        "\\e
           (* Latin: „id est“  meaning „that is to say“. *) 
        #> DOF_lib.define_shortcut \<^binding>\<open>csp\<close>       "CSP"
        #> DOF_lib.define_shortcut \<^binding>\<open>isabelle\<close>  "Isabelle/HOL"\<close> 
-setup\<open>    DOF_lib.define_macro    \<^binding>\<open>vs\<close>        "\\vspace{" "}" (K(K())) \<close> 
 
 (*>*)
 

examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex

@@ -32,11 +32,12 @@
 \newcommand{\ie}{i.e.}
 \newcommand{\eg}{e.g.}
 \newcommand{\etc}{etc}
+\newcommand{\dof}{DOF\xspace}
+
 \newcommand{\path}[1]{\texttt{\nolinkurl{#1}}}
 \title{<TITLE>}
 \author{<AUTHOR>}
 
-\newcommand{\dof}{DOF\xspace}
 \renewcommand{\listofSRACs}{\relax}
 \renewcommand{\listofECs}{\relax}
 \pagestyle{headings}

examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy

@@ -22,7 +22,6 @@ setup \<open>   DOF_lib.define_shortcut \<^binding>\<open>eg\<close>        "\\e
           (* Latin: „id est“  meaning „that is to say“. *) 
        #> DOF_lib.define_shortcut \<^binding>\<open>csp\<close>       "CSP"
        #> DOF_lib.define_shortcut \<^binding>\<open>isabelle\<close>  "Isabelle/HOL"\<close> 
-setup\<open>    DOF_lib.define_macro    \<^binding>\<open>vs\<close>        "\\vspace{" "}" (K(K())) \<close> 
 
 open_monitor*[this::report] 
 (*>*)

src/ontologies/scholarly_paper/scholarly_paper.thy

@@ -418,6 +418,10 @@ fun check_group a = map (check_group_elem (check_level_hd (hd a))) (tl a) ;
 *)
 \<close>
 
+section\<open>Miscelleous: Layout Trimming Commands\<close>
+
+setup\<open>    DOF_lib.define_macro    \<^binding>\<open>hs\<close>        "\\hspace{" "}" (K(K())) \<close> 
+setup\<open>    DOF_lib.define_macro    \<^binding>\<open>vs\<close>        "\\vspace{" "}" (K(K())) \<close> 
 
 end