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