# HG changeset patch
# User nipkow
# Date 1117608265 -7200
# Node ID 833f4160130ee928f07a00eae9bc420834315aff
# Parent  99c3168438ea85bef6555cbcb28e543b2a09b41e
added premise<i>

diff -r 99c3168438ea -r 833f4160130e src/Pure/Isar/term_style.ML
--- a/src/Pure/Isar/term_style.ML	Wed Jun 01 08:44:13 2005 +0200
+++ b/src/Pure/Isar/term_style.ML	Wed Jun 01 08:44:25 2005 +0200
@@ -57,9 +57,24 @@
     | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
   end;
 
+fun premise i _ 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)
+  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 "conclusion" (K Logic.strip_imp_concl)];
 
 end;