...

Isabelle_DOF-Example-II/paper.thy

@@ -751,7 +751,7 @@ This normal form is closed under deterministic and  communication operators.
 The advantage of this format is that we can mimick the well-known product automata construction
 for an arbitrary number of synchronized processes under normal form.
 We only show the case of the synchronous product of two processes: \<close>
-text*[T3::"theorem", short_name="\<open>Product Construction\<close>", level="Some 2"]\<open>
+Theorem*[T3, short_name="\<open>Product Construction\<close>", level="Some 2"]\<open>
 Parallel composition translates to normal form:
 @{cartouche [display,indent=5]\<open>(P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>1,\<upsilon>\<^sub>1\<rbrakk> \<sigma>\<^sub>1) || (P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>2,\<upsilon>\<^sub>2\<rbrakk> \<sigma>\<^sub>2) = 
     P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<lambda>(\<sigma>\<^sub>1,\<sigma>\<^sub>2). \<tau>\<^sub>1 \<sigma>\<^sub>1 \<inter> \<tau>\<^sub>2 \<sigma>\<^sub>2 , \<lambda>(\<sigma>\<^sub>1,\<sigma>\<^sub>2).\<lambda>e.(\<upsilon>\<^sub>1 \<sigma>\<^sub>1 e, \<upsilon>\<^sub>2 \<sigma>\<^sub>2 e)\<rbrakk> (\<sigma>\<^sub>1,\<sigma>\<^sub>2)\<close>}

Isabelle_DOF/thys/manual/M_00_Frontmatter.thy

@@ -36,10 +36,10 @@ define_shortcut* TeXLive \<rightleftharpoons> \<open>\TeXLive\<close>
 text\<open>Note that these setups assume that the associated \<^LaTeX> macros 
      are defined, \<^eg>, in the document prelude. \<close>
 
-define_macro* index  \<rightleftharpoons> \<open>\index{\<close> _ \<open>}\<close>
-define_macro* bindex \<rightleftharpoons> \<open>\bindex{\<close> _ \<open>}\<close>
+define_macro* index     \<rightleftharpoons> \<open>\index{\<close> _ \<open>}\<close>
+define_macro* bindex    \<rightleftharpoons> \<open>\bindex{\<close> _ \<open>}\<close>
 define_macro* nolinkurl \<rightleftharpoons> \<open>\nolinkurl{\<close> _ \<open>}\<close>
-define_macro* center \<rightleftharpoons> \<open>\center{\<close> _ \<open>}\<close>
+define_macro* center    \<rightleftharpoons> \<open>\center{\<close> _ \<open>}\<close>
 define_macro* ltxinline \<rightleftharpoons> \<open>\inlineltx|\<close> _ \<open>|\<close>
 
 

Isabelle_DOF/thys/manual/M_04_RefMan.thy

@@ -1544,7 +1544,7 @@ subsubsection\<open>Restricting the Use of Ontologies to Specific Templates\<clo
 text\<open>
   As ontology representations might rely on features only provided by certain templates 
   (\<^LaTeX>-classes), authors of ontology representations might restrict their use to 
-  specific classes. This can, \<^eg>, be done using the \inlineltx|\@ifclassloaded{}| command:
+  specific classes. This can, \<^eg>, be done using the \<^ltxinline>\<open>\@ifclassloaded{}\<close> command:
 \<^latex>\<open>
 \begin{ltx}
 \@ifclassloaded{llncs}{}%