--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Wed Jun 01 10:40:51 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Wed Jun 01 10:52:17 2005 +0200
@@ -212,17 +212,17 @@
own way, you can extract the premises and the conclusion explicitly
and combine them as you like:
\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 prem1! $thm$\verb!}!
+prints premise 1 of $thm$ (and similarly up to \texttt{prem9}).
\item \verb!@!\verb!{thm_style concl! $thm$\verb!}!
prints the conclusion of $thm$.
\end{itemize}
-For example, ``from @{thm_style premise2 conjI} and
-@{thm_style premise1 conjI} we conclude @{thm_style concl conjI}''
+For example, ``from @{thm_style prem2 conjI} and
+@{thm_style prem1 conjI} we conclude @{thm_style concl conjI}''
is produced by
\begin{quote}
-\verb!from !\verb!@!\verb!{thm_style premise2 conjI}!\\
-\verb!and !\verb!@!\verb!{thm_style premise1 conjI}!\\
+\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}!
\end{quote}
Thus you can rearrange or hide premises and typeset the theorem as you like.
@@ -324,7 +324,7 @@
\end{quote}
A ``style'' is a transformation of propositions. There are predefined
- styles, namly \verb!lhs! and \verb!rhs!, \verb!premise1! unto \verb!premise9!, and \verb!concl!.
+ styles, namly \verb!lhs! and \verb!rhs!, \verb!prem1! up to \verb!prem9!, and \verb!concl!.
For example,
the output
\begin{center}
--- a/src/Pure/Isar/term_style.ML Wed Jun 01 10:40:51 2005 +0200
+++ b/src/Pure/Isar/term_style.ML Wed Jun 01 10:52:17 2005 +0200
@@ -57,24 +57,25 @@
| _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
end;
-fun premise i _ t =
+fun style_parm_premise i ctxt t =
let val prems = Logic.strip_imp_prems t
in if i <= length prems then List.nth(prems, i-1)
- else error ("Not enough premises: premise" ^ string_of_int i)
+ else error ("Not enough premises for prem" ^ string_of_int i ^
+ " in propositon: " ^ ProofContext.string_of_term ctxt t)
end;
-
+
val _ = Context.add_setup
[add_style "lhs" (fst oo style_binargs),
add_style "rhs" (snd oo style_binargs),
- add_style "premise1" (premise 1),
- add_style "premise2" (premise 2),
- add_style "premise3" (premise 3),
- add_style "premise4" (premise 4),
- add_style "premise5" (premise 5),
- add_style "premise6" (premise 6),
- add_style "premise7" (premise 7),
- add_style "premise8" (premise 8),
- add_style "premise9" (premise 9),
+ add_style "prem1" (style_parm_premise 1),
+ add_style "prem2" (style_parm_premise 2),
+ add_style "prem3" (style_parm_premise 3),
+ add_style "prem4" (style_parm_premise 4),
+ add_style "prem5" (style_parm_premise 5),
+ add_style "prem6" (style_parm_premise 6),
+ add_style "prem7" (style_parm_premise 7),
+ add_style "prem8" (style_parm_premise 8),
+ add_style "prem9" (style_parm_premise 9),
add_style "concl" (K Logic.strip_imp_concl)];
end;