renamed premise* to prem
authorhaftmann
Wed Jun 01 10:52:17 2005 +0200 (2005-06-01 ago)
changeset 16167b2e4c4058b71
parent 16166 346bb10d4bbb
child 16168 adb83939177f
renamed premise* to prem
doc-src/LaTeXsugar/Sugar/Sugar.thy
src/Pure/Isar/term_style.ML
     1.1 --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Jun 01 10:40:51 2005 +0200
     1.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Jun 01 10:52:17 2005 +0200
     1.3 @@ -212,17 +212,17 @@
     1.4  own way, you can extract the premises and the conclusion explicitly
     1.5  and combine them as you like:
     1.6  \begin{itemize}
     1.7 -\item \verb!@!\verb!{thm_style premise1! $thm$\verb!}!
     1.8 -prints premise 1 of $thm$ (and similarly up to \texttt{premise9}).
     1.9 +\item \verb!@!\verb!{thm_style prem1! $thm$\verb!}!
    1.10 +prints premise 1 of $thm$ (and similarly up to \texttt{prem9}).
    1.11  \item \verb!@!\verb!{thm_style concl! $thm$\verb!}!
    1.12  prints the conclusion of $thm$.
    1.13  \end{itemize}
    1.14 -For example, ``from @{thm_style premise2 conjI} and
    1.15 -@{thm_style premise1 conjI} we conclude @{thm_style concl conjI}''
    1.16 +For example, ``from @{thm_style prem2 conjI} and
    1.17 +@{thm_style prem1 conjI} we conclude @{thm_style concl conjI}''
    1.18  is produced by
    1.19  \begin{quote}
    1.20 -\verb!from !\verb!@!\verb!{thm_style premise2 conjI}!\\
    1.21 -\verb!and !\verb!@!\verb!{thm_style premise1 conjI}!\\
    1.22 +\verb!from !\verb!@!\verb!{thm_style prem2 conjI}!\\
    1.23 +\verb!and !\verb!@!\verb!{thm_style prem1 conjI}!\\
    1.24  \verb!we conclude !\verb!@!\verb!{thm_style concl conjI}!
    1.25  \end{quote}
    1.26  Thus you can rearrange or hide premises and typeset the theorem as you like.
    1.27 @@ -324,7 +324,7 @@
    1.28      \end{quote}
    1.29  
    1.30    A ``style'' is a transformation of propositions. There are predefined
    1.31 -  styles, namly \verb!lhs! and \verb!rhs!, \verb!premise1! unto \verb!premise9!, and \verb!concl!.
    1.32 +  styles, namly \verb!lhs! and \verb!rhs!, \verb!prem1! up to \verb!prem9!, and \verb!concl!.
    1.33    For example, 
    1.34    the output
    1.35    \begin{center}
     2.1 --- a/src/Pure/Isar/term_style.ML	Wed Jun 01 10:40:51 2005 +0200
     2.2 +++ b/src/Pure/Isar/term_style.ML	Wed Jun 01 10:52:17 2005 +0200
     2.3 @@ -57,24 +57,25 @@
     2.4      | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
     2.5    end;
     2.6  
     2.7 -fun premise i _ t =
     2.8 +fun style_parm_premise i ctxt t =
     2.9    let val prems = Logic.strip_imp_prems t
    2.10    in if i <= length prems then List.nth(prems, i-1)
    2.11 -     else error ("Not enough premises: premise" ^ string_of_int i)
    2.12 +     else error ("Not enough premises for prem" ^ string_of_int i ^
    2.13 +                 " in propositon: " ^ ProofContext.string_of_term ctxt t)
    2.14    end;
    2.15 - 
    2.16 +
    2.17  val _ = Context.add_setup
    2.18   [add_style "lhs" (fst oo style_binargs),
    2.19    add_style "rhs" (snd oo style_binargs),
    2.20 -  add_style "premise1" (premise 1),
    2.21 -  add_style "premise2" (premise 2),
    2.22 -  add_style "premise3" (premise 3),
    2.23 -  add_style "premise4" (premise 4),
    2.24 -  add_style "premise5" (premise 5),
    2.25 -  add_style "premise6" (premise 6),
    2.26 -  add_style "premise7" (premise 7),
    2.27 -  add_style "premise8" (premise 8),
    2.28 -  add_style "premise9" (premise 9),
    2.29 +  add_style "prem1" (style_parm_premise 1),
    2.30 +  add_style "prem2" (style_parm_premise 2),
    2.31 +  add_style "prem3" (style_parm_premise 3),
    2.32 +  add_style "prem4" (style_parm_premise 4),
    2.33 +  add_style "prem5" (style_parm_premise 5),
    2.34 +  add_style "prem6" (style_parm_premise 6),
    2.35 +  add_style "prem7" (style_parm_premise 7),
    2.36 +  add_style "prem8" (style_parm_premise 8),
    2.37 +  add_style "prem9" (style_parm_premise 9),
    2.38    add_style "concl" (K Logic.strip_imp_concl)];
    2.39  
    2.40  end;