--- 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.
--- 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}
*}
--- 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};
--- 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));