--- 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;
-