HOL.ML

   val all_dupE: thm
   val allI: thm
   val arg_cong: thm
   val fun_cong: thm
   val box_equals: thm
+  val case_tac: string -> int -> tactic
   val ccontr: thm
   val classical: thm
   val cong: thm
   val conjunct1: thm
   val conjunct2: thm

 (*Required by the "classical" module*)
 val swap = prove_goal HOL.thy "~P ==> (~Q ==> P) ==> Q"
  (fn major::prems=>
   [ rtac ccontr 1, rtac (major RS notE) 1, REPEAT (ares_tac prems 1)]);
 
+(* case distinction *)
+
+val case_split_thm = prove_goal HOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
+  (fn [p1,p2] => [cut_facts_tac [excluded_middle] 1, etac disjE 1,
+                  etac p2 1, etac p1 1]);
+
+fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
+
 (** Standard abbreviations **)
 
 fun stac th = rtac(th RS ssubst);
 fun sstac ths = EVERY' (map stac ths);
 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
 
 end;
 
 open HOL_Lemmas;
-