diff -r 91614f0eb250 -r ac7b7003f177 HOL.ML
--- a/HOL.ML	Thu Jan 27 17:01:10 1994 +0100
+++ b/HOL.ML	Thu Feb 03 09:55:47 1994 +0100
@@ -17,6 +17,7 @@
   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
@@ -322,6 +323,14 @@
  (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);
@@ -331,4 +340,3 @@
 end;
 
 open HOL_Lemmas;
-