--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu Oct 08 15:59:15 2009 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu Oct 08 15:59:16 2009 +0200
@@ -390,20 +390,20 @@
own way, you can extract the premises and the conclusion explicitly
and combine them as you like:
\begin{itemize}
-\item \verb!@!\verb!{thm_style prem1! $thm$\verb!}!
-prints premise 1 of $thm$ (and similarly up to \texttt{prem9}).
-\item \verb!@!\verb!{thm_style concl! $thm$\verb!}!
+\item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}!
+prints premise 1 of $thm$.
+\item \verb!@!\verb!{thm (concl)! $thm$\verb!}!
prints the conclusion of $thm$.
\end{itemize}
For example, ``from \isa{Q} and
\isa{P} we conclude \isa{P\ {\isasymand}\ Q}''
is produced by
\begin{quote}
-\verb!from !\verb!@!\verb!{thm_style prem2 conjI}! \verb!and !\verb!@!\verb!{thm_style prem1 conjI}!\\
-\verb!we conclude !\verb!@!\verb!{thm_style concl conjI}!
+\verb!from !\verb!@!\verb!{thm (prem 2) conjI}! \verb!and !\verb!@!\verb!{thm (prem 1) conjI}!\\
+\verb!we conclude !\verb!@!\verb!{thm (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
+Styles like !(prem 1)! are a general mechanism explained
in \S\ref{sec:styles}.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -516,12 +516,13 @@
``styles'':
\begin{quote}
- \verb!@!\verb!{thm_style stylename thm}!\\
- \verb!@!\verb!{term_style stylename term}!
+ \verb!@!\verb!{thm (style) thm}!\\
+ \verb!@!\verb!{prop (style) thm}!\\
+ \verb!@!\verb!{term (style) term}!
\end{quote}
A ``style'' is a transformation of propositions. There are predefined
- styles, namely \verb!lhs! and \verb!rhs!, \verb!prem1! up to \verb!prem9!, and \verb!concl!.
+ styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!.
For example,
the output
\begin{center}
@@ -534,8 +535,8 @@
\begin{quote}
\verb!\begin{center}!\\
\verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
- \verb!@!\verb!{thm_style lhs foldl_Nil} & @!\verb!{thm_style rhs foldl_Nil}!\\
- \verb!@!\verb!{thm_style lhs foldl_Cons} & @!\verb!{thm_style rhs foldl_Cons}!\\
+ \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}!\\
+ \verb!@!\verb!{thm (lhs) foldl_Cons} & @!\verb!{thm (rhs) foldl_Cons}!\\
\verb!\end{tabular}!\\
\verb!\end{center}!
\end{quote}
@@ -558,7 +559,7 @@
type
\begin{quote}
\verb!\begin{center}!\\
- \verb!@!\verb!{thm_style [show_types] concl hd_Cons_tl}!\\
+ \verb!@!\verb!{thm [show_types] (concl) hd_Cons_tl}!\\
\verb!\end{center}!
\end{quote}
Beware that any options must be placed \emph{before}
@@ -567,53 +568,7 @@
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!.
- Have a look at the following example:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\begin{isamarkuptext}%
-\begin{quote}
- \verb!setup {!\verb!*!\\
- \verb!let!\\
- \verb! fun my_concl ctxt = Logic.strip_imp_concl!\\
- \verb! in TermStyle.add_style "my_concl" my_concl!\\
- \verb!end;!\\
- \verb!*!\verb!}!\\
- \end{quote}
-
- \noindent
- 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 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
- style has some object-logic specific behaviour for example.
-
- The mapping from identifier name to the style function
- is done by the \verb|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 \isa{hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}.%
+ Have a look at module \verb|Term_Style|.%
\end{isamarkuptext}%
\isamarkuptrue%
%