--- 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!.