# HG changeset patch
# User haftmann
# Date 1117615251 -7200
# Node ID 346bb10d4bbbc48c3dac268b07753ac5f53ee5eb
# Parent  dbe9ee8ffcddf5ed06cd4864648736b67bb43cff
some refinements

diff -r dbe9ee8ffcdd -r 346bb10d4bbb doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Jun 01 10:30:07 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Jun 01 10:40:51 2005 +0200
@@ -206,7 +206,7 @@
 \end{theorem}
 *}
 
-subsection{* Doing it yourself *}
+subsection{* Doing it yourself\label{sec:yourself}*}
 
 text{* If for some reason you want or need to present theorems your
 own way, you can extract the premises and the conclusion explicitly
@@ -324,7 +324,8 @@
     \end{quote}
 
   A ``style'' is a transformation of propositions. There are predefined
-  styles, namly \verb!lhs!, \verb!rhs! and \verb!conclusion!. For example, 
+  styles, namly \verb!lhs! and \verb!rhs!, \verb!premise1! unto \verb!premise9!, and \verb!concl!.
+  For example, 
   the output
   \begin{center}
   \begin{tabular}{l@ {~~@{text "="}~~}l}
@@ -364,6 +365,8 @@
     \verb!\end{center}!
   \end{quote}
 
+  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!.
diff -r dbe9ee8ffcdd -r 346bb10d4bbb doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Wed Jun 01 10:30:07 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Wed Jun 01 10:40:51 2005 +0200
@@ -237,7 +237,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Doing it yourself%
+\isamarkupsubsection{Doing it yourself\label{sec:yourself}%
 }
 \isamarkuptrue%
 %
@@ -248,7 +248,7 @@
 \begin{itemize}
 \item \verb!@!\verb!{thm_style premise1! $thm$\verb!}!
 prints premise 1 of $thm$ (and similarly up to \texttt{premise9}).
-\item \verb!@!\verb!{thm_style conclusion! $thm$\verb!}!
+\item \verb!@!\verb!{thm_style concl! $thm$\verb!}!
 prints the conclusion of $thm$.
 \end{itemize}
 For example, ``from \isa{Q} and
@@ -257,7 +257,7 @@
 \begin{quote}
 \verb!from !\verb!@!\verb!{thm_style premise2 conjI}!\\
 \verb!and !\verb!@!\verb!{thm_style premise1 conjI}!\\
-\verb!we conclude !\verb!@!\verb!{thm_style conclusion conjI}!
+\verb!we conclude !\verb!@!\verb!{thm_style 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
@@ -372,7 +372,8 @@
     \end{quote}
 
   A ``style'' is a transformation of propositions. There are predefined
-  styles, namly \verb!lhs!, \verb!rhs! and \verb!conclusion!. For example, 
+  styles, namly \verb!lhs! and \verb!rhs!, \verb!premise1! unto \verb!premise9!, and \verb!concl!.
+  For example, 
   the output
   \begin{center}
   \begin{tabular}{l@ {~~\isa{{\isacharequal}}~~}l}
@@ -396,7 +397,7 @@
   conclusion of propositions consisting of a binary operator
   (e.~g.~\isa{{\isacharequal}}, \isa{{\isasymequiv}}, \isa{{\isacharless}}).
 
-  Likewise, \verb!conclusion! may be used as a style to show just the
+  Likewise, \verb!concl! 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}
@@ -408,10 +409,12 @@
   type
   \begin{quote}
     \verb!\begin{center}!\\
-    \verb!@!\verb!{thm_style conclusion hd_Cons_tl}!\\
+    \verb!@!\verb!{thm_style concl hd_Cons_tl}!\\
     \verb!\end{center}!
   \end{quote}
 
+  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!.
@@ -431,9 +434,8 @@
   \end{quote}
 
   \noindent
-  This example shows how the \verb!conclusion! style could have been implemented
+  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 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