doc-src/LaTeXsugar/Sugar/document/Sugar.tex

 \begin{isamarkuptext}%
 If for some reason you want or need to present theorems your
 own way, you can extract the premises and the conclusion explicitly
 and combine them as you like:
 \begin{itemize}
-\item \verb!@!\verb!{thm_style prem1! $thm$\verb!}!
-prints premise 1 of $thm$ (and similarly up to \texttt{prem9}).
-\item \verb!@!\verb!{thm_style concl! $thm$\verb!}!
+\item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}!
+prints premise 1 of $thm$.
+\item \verb!@!\verb!{thm (concl)! $thm$\verb!}!
 prints the conclusion of $thm$.
 \end{itemize}
 For example, ``from \isa{Q} and
 \isa{P} we conclude \isa{P\ {\isasymand}\ Q}''
 is produced by
 \begin{quote}
-\verb!from !\verb!@!\verb!{thm_style prem2 conjI}! \verb!and !\verb!@!\verb!{thm_style prem1 conjI}!\\
-\verb!we conclude !\verb!@!\verb!{thm_style concl conjI}!
+\verb!from !\verb!@!\verb!{thm (prem 2) conjI}! \verb!and !\verb!@!\verb!{thm (prem 1) conjI}!\\
+\verb!we conclude !\verb!@!\verb!{thm (concl) conjI}!
 \end{quote}
 Thus you can rearrange or hide premises and typeset the theorem as you like.
-The \verb!thm_style! antiquotation is a general mechanism explained
+Styles like !(prem 1)! are a general mechanism explained
 in \S\ref{sec:styles}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsubsection{Patterns%

   To deal with such cases where it is desirable to dive into the structure
   of terms and theorems, Isabelle offers antiquotations featuring
   ``styles'':
 
     \begin{quote}
-    \verb!@!\verb!{thm_style stylename thm}!\\
-    \verb!@!\verb!{term_style stylename term}!
+    \verb!@!\verb!{thm (style) thm}!\\
+    \verb!@!\verb!{prop (style) thm}!\\
+    \verb!@!\verb!{term (style) term}!
     \end{quote}
 
   A ``style'' is a transformation of propositions. There are predefined
-  styles, namely \verb!lhs! and \verb!rhs!, \verb!prem1! up to \verb!prem9!, and \verb!concl!.
+  styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!.
   For example, 
   the output
   \begin{center}
   \begin{tabular}{l@ {~~\isa{{\isacharequal}}~~}l}
   \isa{foldl\ f\ a\ {\isacharbrackleft}{\isacharbrackright}} & \isa{a}\\

   \end{center}
   is produced by the following code:
   \begin{quote}
     \verb!\begin{center}!\\
     \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
-    \verb!@!\verb!{thm_style lhs foldl_Nil} & @!\verb!{thm_style rhs foldl_Nil}!\\
-    \verb!@!\verb!{thm_style lhs foldl_Cons} & @!\verb!{thm_style rhs foldl_Cons}!\\
+    \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}!\\
+    \verb!@!\verb!{thm (lhs) foldl_Cons} & @!\verb!{thm (rhs) foldl_Cons}!\\
     \verb!\end{tabular}!\\
     \verb!\end{center}!
   \end{quote}
   Note the space between \verb!@! and \verb!{! in the tabular argument.
   It prevents Isabelle from interpreting \verb!@ {~~...~~}! 

     \isa{hd\ {\isacharparenleft}xs\ {\isasymColon}\ {\isacharprime}a\ list{\isacharparenright}{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
   \end{center}
   type
   \begin{quote}
     \verb!\begin{center}!\\
-    \verb!@!\verb!{thm_style [show_types] concl hd_Cons_tl}!\\
+    \verb!@!\verb!{thm [show_types] (concl) hd_Cons_tl}!\\
     \verb!\end{center}!
   \end{quote}
   Beware that any options must be placed \emph{before}
   the name of the style, as in this example.
 
   Further use cases can be found in \S\ref{sec:yourself}.
 
   If you are not afraid of ML, you may also define your own styles.
-  A style is implemented by an ML function of type
-  \verb!Proof.context -> term -> term!.
-  Have a look at the following example:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\begin{isamarkuptext}%
-\begin{quote}
-    \verb!setup {!\verb!*!\\
-    \verb!let!\\
-    \verb!  fun my_concl ctxt = Logic.strip_imp_concl!\\
-    \verb!  in TermStyle.add_style "my_concl" my_concl!\\
-    \verb!end;!\\
-    \verb!*!\verb!}!\\
-  \end{quote}
-
-  \noindent
-  This example shows how the \verb!concl! style is implemented
-  and may be used as as a ``copy-and-paste'' pattern to write your own styles.
-
-  The code should go into your theory file, separate from the \LaTeX\ text.
-  The \verb!let! expression avoids polluting the
-  ML global namespace. Each style receives the current proof context
-  as first argument; this is helpful in situations where the
-  style has some object-logic specific behaviour for example.
-
-  The mapping from identifier name to the style function
-  is done by the \verb|TermStyle.add_style| expression which expects the desired
-  style name and the style function as arguments.
-  
-  After this \verb!setup!,
-  there will be a new style available named \verb!my_concl!, thus allowing
-  antiquoations like \verb!@!\verb!{thm_style my_concl hd_Cons_tl}!
-  yielding \isa{hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}.%
+  Have a look at module \verb|Term_Style|.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isadelimtheory
 %