1.1 --- a/src/FOL/FOL.ML	Fri Jun 24 10:45:02 1994 +0200
     1.2 +++ b/src/FOL/FOL.ML	Fri Jun 24 13:01:53 1994 +0200
     1.3 @@ -12,6 +12,7 @@
     1.4    sig
     1.5    val disjCI : thm
     1.6    val excluded_middle : thm
     1.7 +  val excluded_middle_tac : string -> int -> tactic
     1.8    val exCI : thm
     1.9    val ex_classical : thm
    1.10    val iffCE : thm
    1.11 @@ -52,6 +53,9 @@
    1.12  val excluded_middle = prove_goal FOL.thy "~P | P"
    1.13   (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
    1.14  
    1.15 +(*For disjunctive case analysis*)
    1.16 +fun excluded_middle_tac sP =
    1.17 +    res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
    1.18  
    1.19  (*** Special elimination rules *)
    1.20