diff -r 1314ef1e49dd -r cd4983c76548 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue May 03 10:25:30 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue May 03 10:32:32 2005 +0200
@@ -195,45 +195,6 @@
 \end{theorem}
 *}
 
-subsection {*Definitions and Equations*}
-
-text {*
-  The \verb!thm! antiquotation works nicely for proper theorems, but
-  sets of equations as used in definitions are more difficult to
-  typeset nicely: for some reason people tend to prefer aligned 
-  @{text "="} signs.
-
-  Isabelle2005 has a nice mechanism for this, namely the two
-  antiquotations \verb!@!\verb!{lhs thm}! and \verb!@!\verb!{rhs thm}!.
-
-  \begin{center}
-  \begin{tabular}{l@ {~~@{text "="}~~}l}
-  @{lhs foldl_Nil} & @{rhs foldl_Nil}\\
-  @{lhs foldl_Cons} & @{rhs foldl_Cons}
-  \end{tabular}
-  \end{center}
-
-  \noindent 
-  is produced by the following code:
-
-\begin{quote}
-  \verb!\begin{center}!\\
-  \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
-  \verb!@!\verb!{lhs foldl_Nil} & @!\verb!{rhs foldl_Nil}!\\
-  \verb!@!\verb!{lhs foldl_Cons} & @!\verb!{rhs foldl_Cons}!\\
-  \verb!\end{tabular}!\\
-  \verb!\end{center}!
-\end{quote}
-
-  \noindent
-  Note the space between \verb!@! and \verb!{! in the tabular argument.
-  It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
-  as antiquotation. \verb!@!\verb!{lhs thm}! and \verb!@!\verb!{rhs thm}! 
-  try to be smart about the interpretation of the theorem they
-  print, they work just as well for meta equality @{text "\<equiv>"} and other
-  binary operators like @{text "<"}.
-*}
-
 subsection "Patterns"
 
 text {*
@@ -311,6 +272,105 @@
   
 *}
 
+subsection "Styles"
+
+text {*
+  The \verb!thm! antiquotation works nicely for proper theorems, but
+  sets of equations as used in definitions are more difficult to
+  typeset nicely: for some reason people tend to prefer aligned 
+  @{text "="} signs.
+
+  To deal with such cases where it is desirable to dive into the structure
+  of terms and theorems, Isabelle offers two antiquotations featuring
+  ``styles'':
+
+    \begin{quote}
+    \verb!@!\verb!{thm_style stylename thm}!\\
+    \verb!@!\verb!{term_style stylename term}!
+    \end{quote}
+
+  A ``style'' is a transformation of terms; there are three predefined
+  styles, named \verb!lhs!, \verb!rhs! and \verb!concl!, which obvious
+  meanings, e.~g.~the output
+
+  \begin{center}
+  \begin{tabular}{l@ {~~@{text "="}~~}l}
+  @{thm_style lhs foldl_Nil} & @{thm_style rhs foldl_Nil}\\
+  @{thm_style lhs foldl_Cons} & @{thm_style rhs foldl_Cons}
+  \end{tabular}
+  \end{center}
+
+  \noindent 
+  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!\end{tabular}!\\
+    \verb!\end{center}!
+  \end{quote}
+
+  \noindent
+  Note the space between \verb!@! and \verb!{! in the tabular argument.
+  It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
+  as antiquotation. Both styles \verb!lhs! and \verb!rhs! 
+  try to be smart about the interpretation of the theorem they transform
+  they work just as well for meta equality @{text "\<equiv>"} and other
+  binary operators like @{text "<"}.
+
+  Likewise \verb!conclusion! may be used as style to show just the conclusion
+  of a formula:
+
+  \begin{center}
+    @{thm_style conclusion hd_Cons_tl}
+  \end{center}
+
+  \noindent 
+  is produced by
+
+  \begin{quote}
+    \verb!\begin{center}!\\
+    \verb!@!\verb!{thm_style conclusion hd_Cons_tl}!\\
+    \verb!\end{center}!
+  \end{quote}
+
+  If you aren't afraid about ML, you may also define your own styles;
+  a style is simply implemented by a ML function \verb!Term.term -> Term.term!.
+  Have a look at the following example (which indeed shows just the way the
+  \verb!lhs! style is implemented):
+
+  \begin{quote}
+    \verb!setup {!\verb!*!\\
+    \verb!!\\
+    \verb!let!\\
+    \verb!  fun my_lhs (Const ("==", _) $ t $ _) = t!\\
+    \verb!    | my_lhs (Const ("Trueprop", _) $ t) = my_lhs t!\\
+    \verb!    | my_lhs (Const ("==>", _) $ _ $ t) = my_lhs t!\\
+    \verb!    | my_lhs (_ $ t $ _) = t!\\
+    \verb!    | my_lhs _ = error ("Binary operator expected")!\\
+    \verb!  in [Style.put_style "new_lhs" my_lhs]!\\
+    \verb!end;!\\
+    \verb!!\\
+    \verb!*!\verb!}!\\
+  \end{quote}
+
+  Like in this example, it is recommended to put the definition of the style
+  function into a \verb!let! expression, in order not to pollute the
+  ML global namespace. The mapping from identifier name to the style function
+  is done by the \verb!Style.put_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!new_lhs!, then allowing
+  antiquoations like \verb!@!\verb!{term_style new_lhs rev_map}!
+  yielding \verb!rev (map f xs)!.
+
+  The example above may be used as as a ``copy-and-paste'' pattern to write
+  your own styles; for a description of the constructs used, please refer
+  to the Isabelle reference manual.
+
+*}
+
 (*<*)
 end
 (*>*)
\ No newline at end of file