# HG changeset patch
# User paulson
# Date 900667449 -7200
# Node ID 8fc4fb20d70f3e127a06496d642fd925b99947ce
# Parent  48ca9ef35fb02c042da858ed7de09d7ebf227a90
added case_tac to be like HOL

diff -r 48ca9ef35fb0 -r 8fc4fb20d70f src/FOL/FOL.ML
--- a/src/FOL/FOL.ML	Fri Jul 17 11:23:17 1998 +0200
+++ b/src/FOL/FOL.ML	Fri Jul 17 11:24:09 1998 +0200
@@ -43,6 +43,14 @@
 fun excluded_middle_tac sP =
     res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
 
+qed_goal "case_split_thm" FOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
+  (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
+                  etac p2 1, etac p1 1]);
+
+(*HOL's more natural case analysis tactic*)
+fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
+
+
 (*** Special elimination rules *)