doc-src/LaTeXsugar/Sugar/Sugar.thy

     \verb!@!\verb!{thm_style stylename thm}!\\
     \verb!@!\verb!{term_style stylename term}!
     \end{quote}
 
   A ``style'' is a transformation of propositions. There are predefined
-  styles, namly \verb!lhs!, \verb!rhs! and \verb!conclusion!, with obvious
-  meanings. For example, the output
+  styles, namly \verb!lhs!, \verb!rhs! and \verb!conclusion!. For example, 
+  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}

     \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!@ {~~...~~}! 
-  as an antiquotation. Both styles \verb!lhs! and \verb!rhs!
+  as an antiquotation. The styles \verb!lhs! and \verb!rhs!
   extract the left hand side (or right hand side respectivly) from the
-  conclusion of propositions, consisting of a binary operator
+  conclusion of propositions consisting of a binary operator
   (e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}).
 
-  Likewise \verb!conclusion! may be used as style to show just the conclusion
-  of a proposition. For example, take
+  Likewise, \verb!conclusion! may be used as a style to show just the
+  conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
   \begin{center}
     @{thm hd_Cons_tl}
   \end{center}
-  produced by
-  \begin{quote}
-    \verb!\begin{center}!\\
-    \verb!@!\verb!{thm hd_Cons_tl}!\\
-    \verb!\end{center}!
-  \end{quote}
   To print just the conclusion,
   \begin{center}
     @{thm_style conclusion hd_Cons_tl}
   \end{center}
   type

     \verb!  in [TermStyle.add_style "my_concl" my_concl]!\\
     \verb!end;!\\
     \verb!*!\verb!}!\\
   \end{quote}
 
-  This example indeed shows how the \verb!conclusion! style could is implemented;
-  note that the real implementation is more sophisticated.
-
-  This code should go into your theory file, not as part of your
-  \LaTeX\ text but as a separate command in front of it.
+  \noindent
+  This example shows how the \verb!conclusion! style could have been implemented
+  and may be used as as a ``copy-and-paste'' pattern to write your own styles.
+  (The real implementation of \verb!conclusion! is a bit more sophisticated).
+
+  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 current proof
-  context has an impact on the style (which is the case e.~g.~when the
-  style has some object-logic specific behaviour).
+  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 @{ML_idf 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 @{thm_style my_concl hd_Cons_tl}.
 
-  The example above may be used as as a ``copy-and-paste'' pattern to write
-  your own styles.
-
 *}
 
 (*<*)
 end
 (*>*)