# HG changeset patch
# User kleing
# Date 1117012499 -7200
# Node ID 03e8a88c0b54a84f3170139e0f858dafa174e0c5
# Parent  8852058ecf8dfd35c415013b1a700e116b6aade9
tuned thm_style section

diff -r 8852058ecf8d -r 03e8a88c0b54 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed May 25 10:51:42 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed May 25 11:14:59 2005 +0200
@@ -294,8 +294,8 @@
     \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}\\
@@ -313,22 +313,16 @@
   \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}
@@ -365,16 +359,16 @@
     \verb!*!\verb!}!\\
   \end{quote}
 
-  This example indeed shows how the \verb!conclusion! style could is implemented;
-  note that the real implementation is more sophisticated.
+  \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).
 
-  This code should go into your theory file, not as part of your
-  \LaTeX\ text but as a separate command in front of it.
+  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
@@ -385,9 +379,6 @@
   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.
-
 *}
 
 (*<*)
diff -r 8852058ecf8d -r 03e8a88c0b54 doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Wed May 25 10:51:42 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Wed May 25 11:14:59 2005 +0200
@@ -339,8 +339,8 @@
     \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@ {~~\isa{{\isacharequal}}~~}l}
   \isa{foldl\ f\ a\ {\isacharbrackleft}{\isacharbrackright}} & \isa{a}\\
@@ -358,22 +358,16 @@
   \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.~\isa{{\isacharequal}}, \isa{{\isasymequiv}}, \isa{{\isacharless}}).
 
-  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}
     \isa{xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
   \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}
     \isa{hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
@@ -403,16 +397,16 @@
     \verb!*!\verb!}!\\
   \end{quote}
 
-  This example indeed shows how the \verb!conclusion! style could is implemented;
-  note that the real implementation is more sophisticated.
+  \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).
 
-  This code should go into your theory file, not as part of your
-  \LaTeX\ text but as a separate command in front of it.
+  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 \isa{TermStyle{\isachardot}add{\isacharunderscore}style} expression which expects the desired
@@ -421,10 +415,7 @@
   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}.
-
-  The example above may be used as as a ``copy-and-paste'' pattern to write
-  your own styles.%
+  yielding \isa{hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%