--- a/src/FOL/FOL.thy Sat Jan 20 14:09:23 2007 +0100
+++ b/src/FOL/FOL.thy Sat Jan 20 14:09:27 2007 +0100
@@ -55,13 +55,8 @@
(*For disjunctive case analysis*)
ML {*
- local
- val excluded_middle = thm "excluded_middle"
- val disjE = thm "disjE"
- in
- fun excluded_middle_tac sP =
- res_inst_tac [("Q",sP)] (excluded_middle RS disjE)
- end
+ fun excluded_middle_tac sP =
+ res_inst_tac [("Q",sP)] (@{thm excluded_middle} RS @{thm disjE})
*}
lemma case_split_thm:
@@ -77,11 +72,7 @@
(*HOL's more natural case analysis tactic*)
ML {*
- local
- val case_split_thm = thm "case_split_thm"
- in
- fun case_tac a = res_inst_tac [("P",a)] case_split_thm
- end
+ fun case_tac a = res_inst_tac [("P",a)] @{thm case_split_thm}
*}
@@ -278,10 +269,10 @@
ML {*
structure InductMethod = InductMethodFun
(struct
- val cases_default = thm "case_split";
- val atomize = thms "induct_atomize";
- val rulify = thms "induct_rulify";
- val rulify_fallback = thms "induct_rulify_fallback";
+ val cases_default = @{thm case_split}
+ val atomize = @{thms induct_atomize}
+ val rulify = @{thms induct_rulify}
+ val rulify_fallback = @{thms induct_rulify_fallback}
end);
*}