--- a/src/FOL/FOL.thy Sat Jun 14 23:20:00 2008 +0200
+++ b/src/FOL/FOL.thy Sat Jun 14 23:20:02 2008 +0200
@@ -60,12 +60,6 @@
apply assumption
done
-(*For disjunctive case analysis*)
-ML {*
- fun excluded_middle_tac sP =
- res_inst_tac [("Q",sP)] (@{thm excluded_middle} RS @{thm disjE})
-*}
-
lemma case_split [case_names True False]:
assumes r1: "P ==> Q"
and r2: "~P ==> Q"
@@ -76,9 +70,14 @@
done
ML {*
- fun case_tac a = res_inst_tac [("P",a)] @{thm case_split}
+ fun case_tac ctxt a =
+ RuleInsts.res_inst_tac ctxt [(("P", 0), a)] @{thm case_split}
*}
+method_setup case_tac =
+ {* Method.goal_args_ctxt Args.name case_tac *}
+ "case_tac emulation (dynamic instantiation!)"
+
(*** Special elimination rules *)
@@ -169,7 +168,6 @@
use "cladata.ML"
setup Cla.setup
setup cla_setup
-setup case_setup
use "blastdata.ML"
setup Blast.setup