# HG changeset patch
# User haftmann
# Date 1117614607 -7200
# Node ID dbe9ee8ffcddf5ed06cd4864648736b67bb43cff
# Parent  6b0d68207c140b94547aefe154fb81d885824d04
concl antiqutations

diff -r 6b0d68207c14 -r dbe9ee8ffcdd Admin/makedist
--- 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
 
diff -r 6b0d68207c14 -r dbe9ee8ffcdd doc-src/LaTeXsugar/Sugar/Sugar.thy
--- 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
diff -r 6b0d68207c14 -r dbe9ee8ffcdd src/Pure/Isar/isar_output.ML
--- 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)),
diff -r 6b0d68207c14 -r dbe9ee8ffcdd src/Pure/Isar/term_style.ML
--- 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;