diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy
index 6d235ea..9e5772d 100755
--- a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy
+++ b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy
@@ -26,8 +26,7 @@ define_shortcut* isadof   \<rightleftharpoons> \<open>\isadof\<close>
                  Protege  \<rightleftharpoons> \<open>Prot{\'e}g{\'e}\<close>
 
 (* slanted text in contrast to italics *)
-setup\<open>    DOF_lib.define_macro \<^binding>\<open>slanted_text\<close> "\\textsl{" "}" (K(K()))\<close> 
-
+define_macro* slanted_text \<rightleftharpoons> \<open>\textsl{\<close> \<open>}\<close>
 
 (*>*)
 
diff --git a/examples/scholarly_paper/2020-iFM-CSP/paper.thy b/examples/scholarly_paper/2020-iFM-CSP/paper.thy
index c8cb060..2d4e2d1 100644
--- a/examples/scholarly_paper/2020-iFM-CSP/paper.thy
+++ b/examples/scholarly_paper/2020-iFM-CSP/paper.thy
@@ -1,18 +1,18 @@
 (*<*)
 theory "paper"
-  imports          
-  "Isabelle_DOF.scholarly_paper"
+  imports "Isabelle_DOF.scholarly_paper"
 begin
 
 
 open_monitor*[this::article]
 
-declare[[strict_monitor_checking = false]]
-declare[[ Definition_default_class="definition"]]
-declare[[ Lemma_default_class="lemma"]]
-declare[[ Theorem_default_class="theorem"]]
+declare[[ strict_monitor_checking  = false]]
+declare[[ Definition_default_class = "definition"]]
+declare[[ Lemma_default_class      = "lemma"]]
+declare[[ Theorem_default_class    = "theorem"]]
 
 define_shortcut* csp      \<rightleftharpoons> \<open>CSP\<close>
+                 holcsp   \<rightleftharpoons> \<open>HOL-CSP\<close>
                  isabelle \<rightleftharpoons> \<open>Isabelle/HOL\<close>
 
 (*>*)
@@ -24,7 +24,7 @@ author*[bu,email= "\<open>wolff@lri.fr\<close>",affiliation = "\<open>LRI, Unive
 author*[lina,email="\<open>lina.ye@lri.fr\<close>",affiliation="\<open>LRI, Inria, LSV, CentraleSupelec\<close>"]\<open>Lina Ye\<close>
                
 abstract*[abs, keywordlist="[\<open>Shallow Embedding\<close>,\<open>Process-Algebra\<close>,
-                                   \<open>Concurrency\<close>,\<open>Computational Models\<close>]"]
+                             \<open>Concurrency\<close>,\<open>Computational Models\<close>]"]
 \<open>  The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today 
    one of the reference theories for concurrent specification and computing. In 1997, a first 
    formalization in \<^isabelle> of the denotational semantics of the  Failure/Divergence Model of
@@ -63,8 +63,8 @@ systems, such as the T9000 transansputer @{cite "Barret95"}.
 The theory of \<^csp> was first described in 1978 in a book by Tony Hoare @{cite "Hoare:1985:CSP:3921"}, 
 but has since evolved substantially @{cite "BrookesHR84" and "brookes-roscoe85" and "roscoe:csp:1998"}.
 \<^csp> describes the most common communication and synchronization mechanisms
-with one single language primitive: synchronous communication written \<open>_\<lbrakk>_\<rbrakk>_\<close>. \<^csp> semantics is described 
-by a fully abstract model of behaviour designed to be \<^emph>\<open>compositional\<close>: the denotational
+with one single language primitive: synchronous communication written \<open>_\<lbrakk>_\<rbrakk>_\<close>. \<^csp> semantics is 
+described by a fully abstract model of behaviour designed to be \<^emph>\<open>compositional\<close>: the denotational
 semantics of a process \<open>P\<close> encompasses all possible behaviours of this process in the context of all 
 possible environments \<open>P \<lbrakk>S\<rbrakk> Env\<close> (where \<open>S\<close> is the set of \<open>atomic events\<close> both \<open>P\<close> and \<open>Env\<close> must
 synchronize). This design objective has the consequence that two kinds of choice have to 
@@ -248,7 +248,7 @@ Second, in the traditional literature, the semantic domain is implicitly describ
 over the three semantic functions \<open>\<T>\<close>, \<open>\<F>\<close> and \<open>\<D>\<close>.
 Informally, these are:
 
-   \<^item> the initial trace of a process must be empty; 
+   \<^item> the initial trace of a process must be empty;
    \<^item> any allowed trace must be \<open>front\<^sub>-tickFree\<close>; 
    \<^item> traces of a process are  \<^emph>\<open>prefix-closed\<close>; 
    \<^item> a process can refuse all subsets of a refusal set; 
@@ -272,10 +272,10 @@ Informally, these are:
 (\<forall> s t. s \<in> \<D> P \<and> tickFree s \<and> front_tickFree t \<longrightarrow> s@t \<in> \<D> P)  \<and>
 (\<forall> s X. s \<in> \<D> P \<longrightarrow> (s,X) \<in> \<F> P) \<and>
 (\<forall> s. s@[\<surd>] \<in> \<D> P \<longrightarrow> s \<in> \<D> P)\<close>}
-
 \<^vs>\<open>-0.1cm\<close>
+
 Our objective is to encapsulate this wishlist into a type constructed as a conservative
-theory extension in our theory HOL-\<^csp>.
+theory extension in our theory \<^holcsp>.
 Therefore third, we define a pre-type for processes \<open>\<Sigma> process\<^sub>0\<close> by \<open> \<P>(\<Sigma>\<^sup>\<surd>\<^sup>* \<times> \<P>(\<Sigma>\<^sup>\<surd>)) \<times> \<P>(\<Sigma>\<^sup>\<surd>)\<close>.
 Forth, we turn our wishlist of "axioms" above into the definition of a predicate \<open>is_process P\<close> 
 of type \<open>\<Sigma> process\<^sub>0 \<Rightarrow> bool\<close> deciding if its conditions are fulfilled. Since \<open>P\<close> is a pre-process,
@@ -302,7 +302,7 @@ maintains \<open>is_process\<close>, \<^ie> this predicate remains invariant on
 For example, we define \<open>_\<sqinter>_\<close> on the pre-process type as follows:
 
 \<^vs>\<open>0.1cm\<close>
-  \<^item> \<^theory_text>\<open>definition "P \<sqinter> Q \<equiv> Abs_process(\<F> P \<union> \<F> Q , \<D> P \<union> \<D> Q)"\<close>
+  \<^item> \<^theory_text>\<open>definition "P \<sqinter> Q \<equiv> Abs_processxx(\<F> P \<union> \<F> Q , \<D> P \<union> \<D> Q)"\<close>
 
 \<^vs>\<open>-0.2cm\<close>
 \<^noindent> where \<open>\<F> = fst \<circ> Rep_process\<close> and \<open>\<D> = snd \<circ> Rep_process\<close> and where \<open>Rep_process\<close> and
@@ -532,9 +532,9 @@ To handle termination better, we added two new processes \<open>CHAOS\<^sub>S\<^
 \<close>
 
 (*<*) (* a test ...*)
-text*[X22 ::math_content   ]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close>                                             \<^vs>\<open>-0.7cm\<close> \<close>
-text*[X32::"definition", mcc=defn]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))                   \<^vs>\<open>-0.7cm\<close>\<close>\<close>
-Definition*[X42]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>  \<^vs>\<open>-0.7cm\<close>\<close>
+text*[X22 ::math_content   ]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close>                           \<^vs>\<open>-0.7cm\<close>\<close>
+text*[X32::"definition", mcc=defn]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>        \<^vs>\<open>-0.7cm\<close>\<close>
+Definition*[X42]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>                \<^vs>\<open>-0.7cm\<close>\<close>
 Definition*[X52::"definition"]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>  \<^vs>\<open>-0.7cm\<close>\<close>
 
 text\<open> The \<open>RUN\<close>-process defined @{math_content X22} represents the process that accepts all 
@@ -546,21 +546,19 @@ stops or accepts any offered event, whereas \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I
 Definition*[X2]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close>                       \<^vs>\<open>-0.7cm\<close>\<close>
 Definition*[X3]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>          \<^vs>\<open>-0.7cm\<close>\<close>
 Definition*[X4]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>\<^vs>\<open>-0.7cm\<close>\<close>
-Definition*[X5]\<open>\<open>DF A \<equiv> \<mu> X. (\<sqinter> x \<in> A \<rightarrow> X)\<close>                      \<^vs>\<open>-0.7cm\<close>\<close>
-Definition*[X6]\<open>\<open>DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. ((\<sqinter> x \<in> A \<rightarrow> X) \<sqinter> SKIP)\<close>          \<^vs>\<open>-0.7cm\<close> \<close> 
+Definition*[X5]\<open>\<open>DF A \<equiv> \<mu> X. (\<sqinter> x \<in> A \<rightarrow> X)\<close>                       \<^vs>\<open>-0.7cm\<close>\<close>
+Definition*[X6]\<open>\<open>DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. ((\<sqinter> x \<in> A \<rightarrow> X) \<sqinter> SKIP)\<close>           \<^vs>\<open>-0.7cm\<close> \<close> 
 
-text\<open> \<^vs>\<open>-0.3cm\<close> \<^noindent>
-In the following, we denote \<open> \<R>\<P> = {DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P, DF, RUN, CHAOS, CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P}\<close>. 
+text\<open> \<^vs>\<open>-0.3cm\<close> \<^noindent> In the following, we denote \<open> \<R>\<P> = {DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P, DF, RUN, CHAOS, CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P}\<close>. 
 All five  reference processes are divergence-free.
 %which was done by using a particular lemma \<open>\<D> (\<mu> x. f x) = \<Inter>\<^sub>i\<^sub>\<in>\<^sub>\<nat> \<D> (f\<^sup>i \<bottom>)\<close>.  
-
-\<^vs>\<open>-0.2cm\<close>
-   @{cartouche [display,indent=8] \<open> D (\<PP> UNIV) = {} where \<PP> \<in> \<R>\<P> and UNIV is the set of all events\<close>}
-
-\<^vs>\<open>-0.1cm\<close>
+@{cartouche 
+  [display,indent=8] \<open> D (\<PP> UNIV) = {} where \<PP> \<in> \<R>\<P> and UNIV is the set of all events\<close>
+}
 Regarding the failure refinement ordering, the set of failures \<open>\<F> P\<close> for any process \<open>P\<close> is
 a subset of  \<open>\<F> (CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV)\<close>.% and the following lemma was proved: 
-% This proof is performed by induction, based on the failure projection of \<open>STOP\<close> and that of internal choice.
+% This proof is performed by induction, based on the failure projection of \<open>STOP\<close> and that of 
+% internal choice.
 
 \<^vs>\<open>-0.2cm\<close>
    @{cartouche [display, indent=25] \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<F> P\<close>}
diff --git a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy
index 2456605..db1d713 100755
--- a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy
+++ b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy
@@ -17,13 +17,11 @@ theory "00_Frontmatter"
 begin
 
 
-section\<open>Document Local Setup.\<close>
-text\<open>Some internal setup, introducing document specific abbreviations and macros.\<close>
+section\<open>Local Document Setup.\<close>
+text\<open>... introducing document specific abbreviations and macros.\<close>
 
-
-
-define_shortcut* dof    \<rightleftharpoons> \<open>\dof\<close>
-                 isadof \<rightleftharpoons> \<open>\isadof\<close>
+define_shortcut* dof     \<rightleftharpoons> \<open>\dof\<close>
+                 isadof  \<rightleftharpoons> \<open>\isadof\<close>
 
 define_shortcut* TeXLive \<rightleftharpoons> \<open>\TeXLive\<close>
                  BibTeX  \<rightleftharpoons> \<open>\BibTeX{}\<close> 
@@ -32,11 +30,11 @@ define_shortcut* TeXLive \<rightleftharpoons> \<open>\TeXLive\<close>
                  pdf     \<rightleftharpoons> \<open>PDF\<close>
                  pdftex  \<rightleftharpoons> \<open>\pdftex{}\<close>
 
-text\<open>Note that these setups assume that the associated \<^LaTeX> macros are defined, \<^eg>, 
-     in the document prelude. \<close>
+text\<open>Note that these setups assume that the associated \<^LaTeX> macros 
+     are defined, \<^eg>, in the document prelude. \<close>
 
-setup\<open>    DOF_lib.define_macro \<^binding>\<open>index\<close>   "\\index{" "}" (K(K())) (*no checking, no reporting*)
-       #> DOF_lib.define_macro \<^binding>\<open>bindex\<close>  "\\bindex{" "}"(K(K()))\<close> 
+define_macro* index \<rightleftharpoons> \<open>\index{\<close> \<open>}\<close>
+define_macro* bindex \<rightleftharpoons> \<open>\bindex{\<close> \<open>}\<close>
 
 
 ML\<open>
diff --git a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy
index a918c59..4377317 100755
--- a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy
+++ b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy
@@ -22,7 +22,7 @@ chapter*[isadof_developers::text_section]\<open>Extending \<^isadof>\<close>
 text\<open>
   In this chapter, we describe the basic implementation aspects of \<^isadof>, which is based on 
   the following design-decisions:
-  \<^item> the entire \<^isadof> is a ``pure add-on,'' \ie, we deliberately resign on the possibility to 
+  \<^item> the entire \<^isadof> is a ``pure add-on,'' \<^ie>, we deliberately resign on the possibility to 
     modify Isabelle itself.
   \<^item> we made a small exception to this rule: the \<^isadof> package modifies in its installation 
     about 10 lines in the \LaTeX-generator (\path{src/patches/thy_output.ML}).
diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy
index baea21a..d43998a 100755
--- a/src/DOF/Isa_COL.thy
+++ b/src/DOF/Isa_COL.thy
@@ -29,7 +29,7 @@ theory Isa_COL
   and      "figure*" "side_by_side_figure*"   :: document_body 
   and      "assert*" :: thy_decl
           
-  and      "define_shortcut*" :: thy_decl
+  and      "define_shortcut*" "define_macro*":: thy_decl
 
 begin
   
@@ -293,9 +293,9 @@ fun define_macro name s1 s2 reportNtest =
 
 local (* hide away really strange local construction *)
 fun enclose_body2 front body1 middle body2 post =
-  (if front = "" then [] else [Latex.string front]) @ body1 @
+  (if front  = "" then [] else [Latex.string front]) @ body1 @
   (if middle = "" then [] else [Latex.string middle]) @ body2 @
-  (if post = "" then [] else [Latex.string post]);
+  (if post   = "" then [] else [Latex.string post]);
 in
 fun define_macro2 name front middle post reportNtest1 reportNtest2 =
       Thy_Output.antiquotation_raw_embedded name (Scan.lift (   Args.cartouche_input 
@@ -416,19 +416,33 @@ end
 
 ML\<open>
 local 
-val parse_define_shortcut = Parse.binding -- 
-                            ((\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>) |-- (Parse.alt_string || Parse.cartouche))
+val parse_literal = Parse.alt_string || Parse.cartouche
+val parse_define_shortcut = Parse.binding -- ((\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>) |-- parse_literal)
 val define_shortcuts = fold(uncurry DOF_lib.define_shortcut)
 in
-val _ =
-  Outer_Syntax.command \<^command_keyword>\<open>define_shortcut*\<close> "define LaTeX shortcut"
-    (Scan.repeat1 parse_define_shortcut >> (Toplevel.theory o define_shortcuts));
+val _ =  Outer_Syntax.command \<^command_keyword>\<open>define_shortcut*\<close> "define LaTeX shortcut"
+            (Scan.repeat1 parse_define_shortcut >> (Toplevel.theory o define_shortcuts));
 end
 \<close>
 
+ML\<open>
+val parse_literal = Parse.alt_string || Parse.cartouche
+val parse_define_shortcut = (Parse.binding 
+                             -- ((\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>) |-- parse_literal))
+                             -- parse_literal
+                             -- (Scan.option (\<^keyword>\<open>(\<close> |-- Parse.ML_source --|\<^keyword>\<open>)\<close>))
+
+fun define_macro (X,NONE) = (uncurry(uncurry(uncurry DOF_lib.define_macro)))(X,K(K()));
+
+
+val _ =  Outer_Syntax.command \<^command_keyword>\<open>define_macro*\<close> "define LaTeX shortcut"
+            (Scan.repeat1 parse_define_shortcut >> (Toplevel.theory o (fold define_macro)));
+
+\<close>
+
+
 section\<open>Tables\<close>
 (* TODO ! ! ! *)
-
 (* dito the future monitor: table - block *)
 
 
diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy
index 8f04f55..59e3210 100755
--- a/src/ontologies/scholarly_paper/scholarly_paper.thy
+++ b/src/ontologies/scholarly_paper/scholarly_paper.thy
@@ -477,12 +477,17 @@ subsection\<open>Common Abbreviations\<close>
 
 define_shortcut* eg  \<rightleftharpoons> \<open>\eg\<close>  (* Latin: „exempli gratia“  meaning  „for example“. *)
                  ie  \<rightleftharpoons> \<open>\ie\<close>  (* Latin: „id est“  meaning „that is to say“. *)
-                 etc \<rightleftharpoons> \<open>\etc\<close> (* Latin : et cetera *)
+                 etc \<rightleftharpoons> \<open>\etc\<close> (* Latin : „et cetera“ meaning „et cetera“ *)
 
 subsection\<open>Layout Trimming Commands\<close>
 
+define_macro* hs \<rightleftharpoons> \<open>\hspace{\<close> \<open>}\<close>
+define_macro* vs \<rightleftharpoons> \<open>\vspace{\<close> \<open>}\<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> 
+*)
 
 define_shortcut* clearpage \<rightleftharpoons> \<open>\clearpage{}\<close>