1.1 --- a/Admin/makedist	Wed Jun 01 09:46:06 2005 +0200
     1.2 +++ b/Admin/makedist	Wed Jun 01 10:30:07 2005 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4      export CVSROOT=/usr/proj/isabelle-repository/archive
     1.5      ;;
     1.6    *)
     1.7 -    export CVSROOT=sunbroy2.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/archive       
     1.8 +    export CVSROOT=sunbroy2.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/archive
     1.9      ;;
    1.10  esac
    1.11  

     2.1 --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Jun 01 09:46:06 2005 +0200
     2.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Jun 01 10:30:07 2005 +0200
     2.3 @@ -214,16 +214,16 @@
     2.4  \begin{itemize}
     2.5  \item \verb!@!\verb!{thm_style premise1! $thm$\verb!}!
     2.6  prints premise 1 of $thm$ (and similarly up to \texttt{premise9}).
     2.7 -\item \verb!@!\verb!{thm_style conclusion! $thm$\verb!}!
     2.8 +\item \verb!@!\verb!{thm_style concl! $thm$\verb!}!
     2.9  prints the conclusion of $thm$.
    2.10  \end{itemize}
    2.11  For example, ``from @{thm_style premise2 conjI} and
    2.12 -@{thm_style premise1 conjI} we conclude @{thm_style conclusion conjI}''
    2.13 +@{thm_style premise1 conjI} we conclude @{thm_style concl conjI}''
    2.14  is produced by
    2.15  \begin{quote}
    2.16  \verb!from !\verb!@!\verb!{thm_style premise2 conjI}!\\
    2.17  \verb!and !\verb!@!\verb!{thm_style premise1 conjI}!\\
    2.18 -\verb!we conclude !\verb!@!\verb!{thm_style conclusion conjI}!
    2.19 +\verb!we conclude !\verb!@!\verb!{thm_style concl conjI}!
    2.20  \end{quote}
    2.21  Thus you can rearrange or hide premises and typeset the theorem as you like.
    2.22  The \verb!thm_style! antiquotation is a general mechanism explained
    2.23 @@ -348,19 +348,19 @@
    2.24    conclusion of propositions consisting of a binary operator
    2.25    (e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}).
    2.26  
    2.27 -  Likewise, \verb!conclusion! may be used as a style to show just the
    2.28 +  Likewise, \verb!concl! may be used as a style to show just the
    2.29    conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
    2.30    \begin{center}
    2.31      @{thm hd_Cons_tl}
    2.32    \end{center}
    2.33    To print just the conclusion,
    2.34    \begin{center}
    2.35 -    @{thm_style conclusion hd_Cons_tl}
    2.36 +    @{thm_style concl hd_Cons_tl}
    2.37    \end{center}
    2.38    type
    2.39    \begin{quote}
    2.40      \verb!\begin{center}!\\
    2.41 -    \verb!@!\verb!{thm_style conclusion hd_Cons_tl}!\\
    2.42 +    \verb!@!\verb!{thm_style concl hd_Cons_tl}!\\
    2.43      \verb!\end{center}!
    2.44    \end{quote}
    2.45  
    2.46 @@ -390,9 +390,8 @@
    2.47    \end{quote}
    2.48  
    2.49    \noindent
    2.50 -  This example shows how the \verb!conclusion! style could have been implemented
    2.51 +  This example shows how the \verb!concl! style is implemented
    2.52    and may be used as as a ``copy-and-paste'' pattern to write your own styles.
    2.53 -  (The real implementation of \verb!conclusion! is a bit more sophisticated).
    2.54  
    2.55    The code should go into your theory file, separate from the \LaTeX\ text.
    2.56    The \verb!let! expression avoids polluting the

     3.1 --- a/src/Pure/Isar/isar_output.ML	Wed Jun 01 09:46:06 2005 +0200
     3.2 +++ b/src/Pure/Isar/isar_output.ML	Wed Jun 01 10:30:07 2005 +0200
     3.3 @@ -394,10 +394,10 @@
     3.4  
     3.5  val _ = add_commands
     3.6   [("thm", args Attrib.local_thmss (output_seq_with pretty_thm)),
     3.7 -  ("thm_style", args ((Scan.lift Args.name) -- Attrib.local_thm) (output_with pretty_thm_style)),
     3.8 +  ("thm_style", args ((Scan.lift (Args.name || Args.symbol)) -- Attrib.local_thm) (output_with pretty_thm_style)),
     3.9    ("prop", args Args.local_prop (output_with pretty_term)),
    3.10    ("term", args Args.local_term (output_with pretty_term)),
    3.11 -  ("term_style", args ((Scan.lift Args.name) -- Args.local_term) (output_with pretty_term_style)),
    3.12 +  ("term_style", args ((Scan.lift (Args.name || Args.symbol)) -- Args.local_term) (output_with pretty_term_style)),
    3.13    ("term_type", args Args.local_term (output_with pretty_term_typ)),
    3.14    ("typeof", args Args.local_term (output_with pretty_term_typeof)),
    3.15    ("const", args Args.local_term (output_with pretty_term_const)),

     4.1 --- a/src/Pure/Isar/term_style.ML	Wed Jun 01 09:46:06 2005 +0200
     4.2 +++ b/src/Pure/Isar/term_style.ML	Wed Jun 01 10:30:07 2005 +0200
     4.3 @@ -59,7 +59,7 @@
     4.4  
     4.5  fun premise i _ t =
     4.6    let val prems = Logic.strip_imp_prems t
     4.7 -  in if i <= length prems then List.nth(prems,i-1)
     4.8 +  in if i <= length prems then List.nth(prems, i-1)
     4.9       else error ("Not enough premises: premise" ^ string_of_int i)
    4.10    end;
    4.11   
    4.12 @@ -75,6 +75,6 @@
    4.13    add_style "premise7" (premise 7),
    4.14    add_style "premise8" (premise 8),
    4.15    add_style "premise9" (premise 9),
    4.16 -  add_style "conclusion" (K Logic.strip_imp_concl)];
    4.17 +  add_style "concl" (K Logic.strip_imp_concl)];
    4.18  
    4.19  end;