--- a/Admin/makedist Wed Jun 01 09:46:06 2005 +0200
+++ b/Admin/makedist Wed Jun 01 10:30:07 2005 +0200
@@ -17,7 +17,7 @@
export CVSROOT=/usr/proj/isabelle-repository/archive
;;
*)
- export CVSROOT=sunbroy2.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/archive
+ export CVSROOT=sunbroy2.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/archive
;;
esac
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Wed Jun 01 09:46:06 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Wed Jun 01 10:30:07 2005 +0200
@@ -214,16 +214,16 @@
\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 @{thm_style premise2 conjI} and
-@{thm_style premise1 conjI} we conclude @{thm_style conclusion conjI}''
+@{thm_style premise1 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!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
@@ -348,19 +348,19 @@
conclusion of propositions consisting of a binary operator
(e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}).
- 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}
@{thm hd_Cons_tl}
\end{center}
To print just the conclusion,
\begin{center}
- @{thm_style conclusion hd_Cons_tl}
+ @{thm_style concl hd_Cons_tl}
\end{center}
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}
@@ -390,9 +390,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
--- a/src/Pure/Isar/isar_output.ML Wed Jun 01 09:46:06 2005 +0200
+++ b/src/Pure/Isar/isar_output.ML Wed Jun 01 10:30:07 2005 +0200
@@ -394,10 +394,10 @@
val _ = add_commands
[("thm", args Attrib.local_thmss (output_seq_with pretty_thm)),
- ("thm_style", args ((Scan.lift Args.name) -- Attrib.local_thm) (output_with pretty_thm_style)),
+ ("thm_style", args ((Scan.lift (Args.name || Args.symbol)) -- Attrib.local_thm) (output_with pretty_thm_style)),
("prop", args Args.local_prop (output_with pretty_term)),
("term", args Args.local_term (output_with pretty_term)),
- ("term_style", args ((Scan.lift Args.name) -- Args.local_term) (output_with pretty_term_style)),
+ ("term_style", args ((Scan.lift (Args.name || Args.symbol)) -- Args.local_term) (output_with pretty_term_style)),
("term_type", args Args.local_term (output_with pretty_term_typ)),
("typeof", args Args.local_term (output_with pretty_term_typeof)),
("const", args Args.local_term (output_with pretty_term_const)),
--- a/src/Pure/Isar/term_style.ML Wed Jun 01 09:46:06 2005 +0200
+++ b/src/Pure/Isar/term_style.ML Wed Jun 01 10:30:07 2005 +0200
@@ -59,7 +59,7 @@
fun premise i _ t =
let val prems = Logic.strip_imp_prems t
- in if i <= length prems then List.nth(prems,i-1)
+ in if i <= length prems then List.nth(prems, i-1)
else error ("Not enough premises: premise" ^ string_of_int i)
end;
@@ -75,6 +75,6 @@
add_style "premise7" (premise 7),
add_style "premise8" (premise 8),
add_style "premise9" (premise 9),
- add_style "conclusion" (K Logic.strip_imp_concl)];
+ add_style "concl" (K Logic.strip_imp_concl)];
end;