# HG changeset patch
# User wenzelm
# Date 1213108981 -7200
# Node ID 0dcafa5c9e3fc7bc4265989a7d0e690fecba832e
# Parent  22e8c115f6c949934d375d7aceba5399d02b036d
eliminated obsolete case_split_thm -- use case_split;

diff -r 22e8c115f6c9 -r 0dcafa5c9e3f doc-src/IsarOverview/Isar/Induction.thy
--- a/doc-src/IsarOverview/Isar/Induction.thy	Tue Jun 10 16:42:38 2008 +0200
+++ b/doc-src/IsarOverview/Isar/Induction.thy	Tue Jun 10 16:43:01 2008 +0200
@@ -24,11 +24,11 @@
 qed
 
 text{*\noindent The two cases must come in this order because @{text
-cases} merely abbreviates @{text"(rule case_split_thm)"} where
-@{thm[source] case_split_thm} is @{thm case_split_thm}. If we reverse
+cases} merely abbreviates @{text"(rule case_split)"} where
+@{thm[source] case_split} is @{thm case_split}. If we reverse
 the order of the two cases in the proof, the first case would prove
 @{prop"\<not> A \<Longrightarrow> \<not> A \<or> A"} which would solve the first premise of
-@{thm[source] case_split_thm}, instantiating @{text ?P} with @{term "\<not>
+@{thm[source] case_split}, instantiating @{text ?P} with @{term "\<not>
 A"}, thus making the second premise @{prop"\<not> \<not> A \<Longrightarrow> \<not> A \<or> A"}.
 Therefore the order of subgoals is not always completely arbitrary.
 
diff -r 22e8c115f6c9 -r 0dcafa5c9e3f src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Tue Jun 10 16:42:38 2008 +0200
+++ b/src/FOL/FOL.thy	Tue Jun 10 16:43:01 2008 +0200
@@ -66,7 +66,7 @@
     res_inst_tac [("Q",sP)] (@{thm excluded_middle} RS @{thm disjE})
 *}
 
-lemma case_split_thm:
+lemma case_split [case_names True False]:
   assumes r1: "P ==> Q"
     and r2: "~P ==> Q"
   shows Q
@@ -75,11 +75,8 @@
   apply (erule r1)
   done
 
-lemmas case_split = case_split_thm [case_names True False]
-
-(*HOL's more natural case analysis tactic*)
 ML {*
-  fun case_tac a = res_inst_tac [("P",a)] @{thm case_split_thm}
+  fun case_tac a = res_inst_tac [("P",a)] @{thm case_split}
 *}
 
 
diff -r 22e8c115f6c9 -r 0dcafa5c9e3f src/HOL/Tools/function_package/fundef_core.ML
--- a/src/HOL/Tools/function_package/fundef_core.ML	Tue Jun 10 16:42:38 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Tue Jun 10 16:43:01 2008 +0200
@@ -103,7 +103,7 @@
 
 val acc_downward = @{thm accp_downward};
 val accI = @{thm accp.accI};
-val case_split = @{thm HOL.case_split_thm};
+val case_split = @{thm HOL.case_split};
 val fundef_default_value = @{thm FunDef.fundef_default_value};
 val not_acc_down = @{thm not_accp_down};
 
diff -r 22e8c115f6c9 -r 0dcafa5c9e3f src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Tue Jun 10 16:42:38 2008 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Tue Jun 10 16:43:01 2008 +0200
@@ -75,7 +75,7 @@
 		val Q     = Var (("Q", 0), HOLogic.boolT)
 		val False = HOLogic.false_const
 	in
-		Thm.instantiate ([], [(cterm Q, cterm False)]) case_split_thm
+		Thm.instantiate ([], [(cterm Q, cterm False)]) @{thm case_split}
 	end;
 
 val cP = cterm_of (theory_of_thm resolution_thm) (Var (("P", 0), HOLogic.boolT));