src/Pure/Isar/term_style.ML
changeset 16160 833f4160130e
parent 15990 4ef32dcbb44f
child 16165 dbe9ee8ffcdd
     1.1 --- a/src/Pure/Isar/term_style.ML	Wed Jun 01 08:44:13 2005 +0200
     1.2 +++ b/src/Pure/Isar/term_style.ML	Wed Jun 01 08:44:25 2005 +0200
     1.3 @@ -57,9 +57,24 @@
     1.4      | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
     1.5    end;
     1.6  
     1.7 +fun premise i _ t =
     1.8 +  let val prems = Logic.strip_imp_prems t
     1.9 +  in if i <= length prems then List.nth(prems,i-1)
    1.10 +     else error ("Not enough premises: premise" ^ string_of_int i)
    1.11 +  end;
    1.12 + 
    1.13  val _ = Context.add_setup
    1.14   [add_style "lhs" (fst oo style_binargs),
    1.15    add_style "rhs" (snd oo style_binargs),
    1.16 +  add_style "premise1" (premise 1),
    1.17 +  add_style "premise2" (premise 2),
    1.18 +  add_style "premise3" (premise 3),
    1.19 +  add_style "premise4" (premise 4),
    1.20 +  add_style "premise5" (premise 5),
    1.21 +  add_style "premise6" (premise 6),
    1.22 +  add_style "premise7" (premise 7),
    1.23 +  add_style "premise8" (premise 8),
    1.24 +  add_style "premise9" (premise 9),
    1.25    add_style "conclusion" (K Logic.strip_imp_concl)];
    1.26  
    1.27  end;