--- 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);
*}
--- a/src/FOL/IFOL.thy Sat Jan 20 14:09:23 2007 +0100
+++ b/src/FOL/IFOL.thy Sat Jan 20 14:09:27 2007 +0100
@@ -231,13 +231,8 @@
(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
ML {*
- local
- val notE = thm "notE"
- val impE = thm "impE"
- in
- fun mp_tac i = eresolve_tac [notE,impE] i THEN assume_tac i
- fun eq_mp_tac i = eresolve_tac [notE,impE] i THEN eq_assume_tac i
- end
+ fun mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i THEN assume_tac i
+ fun eq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i THEN eq_assume_tac i
*}
@@ -337,14 +332,9 @@
(*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*)
ML {*
- local
- val iffE = thm "iffE"
- val mp = thm "mp"
- in
- fun iff_tac prems i =
- resolve_tac (prems RL [iffE]) i THEN
- REPEAT1 (eresolve_tac [asm_rl, mp] i)
- end
+ fun iff_tac prems i =
+ resolve_tac (prems RL @{thms iffE}) i THEN
+ REPEAT1 (eresolve_tac [@{thm asm_rl}, @{thm mp}] i)
*}
lemma conj_cong:
@@ -525,7 +515,7 @@
bind_thms ("pred_congs",
List.concat (map (fn c =>
map (fn th => read_instantiate [("P",c)] th)
- [thm "pred1_cong", thm "pred2_cong", thm "pred3_cong"])
+ [@{thm pred1_cong}, @{thm pred2_cong}, @{thm pred3_cong}])
(explode"PQRS")))
*}
@@ -614,9 +604,9 @@
ML {*
structure ProjectRule = ProjectRuleFun
(struct
- val conjunct1 = thm "conjunct1";
- val conjunct2 = thm "conjunct2";
- val mp = thm "mp";
+ val conjunct1 = @{thm conjunct1}
+ val conjunct2 = @{thm conjunct2}
+ val mp = @{thm mp}
end)
*}
@@ -791,41 +781,41 @@
subsection {* ML bindings *}
ML {*
-val refl = thm "refl"
-val trans = thm "trans"
-val sym = thm "sym"
-val subst = thm "subst"
-val ssubst = thm "ssubst"
-val conjI = thm "conjI"
-val conjE = thm "conjE"
-val conjunct1 = thm "conjunct1"
-val conjunct2 = thm "conjunct2"
-val disjI1 = thm "disjI1"
-val disjI2 = thm "disjI2"
-val disjE = thm "disjE"
-val impI = thm "impI"
-val impE = thm "impE"
-val mp = thm "mp"
-val rev_mp = thm "rev_mp"
-val TrueI = thm "TrueI"
-val FalseE = thm "FalseE"
-val iff_refl = thm "iff_refl"
-val iff_trans = thm "iff_trans"
-val iffI = thm "iffI"
-val iffE = thm "iffE"
-val iffD1 = thm "iffD1"
-val iffD2 = thm "iffD2"
-val notI = thm "notI"
-val notE = thm "notE"
-val allI = thm "allI"
-val allE = thm "allE"
-val spec = thm "spec"
-val exI = thm "exI"
-val exE = thm "exE"
-val eq_reflection = thm "eq_reflection"
-val iff_reflection = thm "iff_reflection"
-val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq"
-val meta_eq_to_iff = thm "meta_eq_to_iff"
+val refl = @{thm refl}
+val trans = @{thm trans}
+val sym = @{thm sym}
+val subst = @{thm subst}
+val ssubst = @{thm ssubst}
+val conjI = @{thm conjI}
+val conjE = @{thm conjE}
+val conjunct1 = @{thm conjunct1}
+val conjunct2 = @{thm conjunct2}
+val disjI1 = @{thm disjI1}
+val disjI2 = @{thm disjI2}
+val disjE = @{thm disjE}
+val impI = @{thm impI}
+val impE = @{thm impE}
+val mp = @{thm mp}
+val rev_mp = @{thm rev_mp}
+val TrueI = @{thm TrueI}
+val FalseE = @{thm FalseE}
+val iff_refl = @{thm iff_refl}
+val iff_trans = @{thm iff_trans}
+val iffI = @{thm iffI}
+val iffE = @{thm iffE}
+val iffD1 = @{thm iffD1}
+val iffD2 = @{thm iffD2}
+val notI = @{thm notI}
+val notE = @{thm notE}
+val allI = @{thm allI}
+val allE = @{thm allE}
+val spec = @{thm spec}
+val exI = @{thm exI}
+val exE = @{thm exE}
+val eq_reflection = @{thm eq_reflection}
+val iff_reflection = @{thm iff_reflection}
+val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq}
+val meta_eq_to_iff = @{thm meta_eq_to_iff}
*}
end
--- a/src/HOL/Lattices.thy Sat Jan 20 14:09:23 2007 +0100
+++ b/src/HOL/Lattices.thy Sat Jan 20 14:09:27 2007 +0100
@@ -280,26 +280,26 @@
text {* ML legacy bindings *}
ML {*
-val Least_def = thm "Least_def";
-val Least_equality = thm "Least_equality";
-val min_def = thm "min_def";
-val min_of_mono = thm "min_of_mono";
-val max_def = thm "max_def";
-val max_of_mono = thm "max_of_mono";
-val min_leastL = thm "min_leastL";
-val max_leastL = thm "max_leastL";
-val min_leastR = thm "min_leastR";
-val max_leastR = thm "max_leastR";
-val le_max_iff_disj = thm "le_max_iff_disj";
-val le_maxI1 = thm "le_maxI1";
-val le_maxI2 = thm "le_maxI2";
-val less_max_iff_disj = thm "less_max_iff_disj";
-val max_less_iff_conj = thm "max_less_iff_conj";
-val min_less_iff_conj = thm "min_less_iff_conj";
-val min_le_iff_disj = thm "min_le_iff_disj";
-val min_less_iff_disj = thm "min_less_iff_disj";
-val split_min = thm "split_min";
-val split_max = thm "split_max";
+val Least_def = @{thm Least_def}
+val Least_equality = @{thm Least_equality}
+val min_def = @{thm min_def}
+val min_of_mono = @{thm min_of_mono}
+val max_def = @{thm max_def}
+val max_of_mono = @{thm max_of_mono}
+val min_leastL = @{thm min_leastL}
+val max_leastL = @{thm max_leastL}
+val min_leastR = @{thm min_leastR}
+val max_leastR = @{thm max_leastR}
+val le_max_iff_disj = @{thm le_max_iff_disj}
+val le_maxI1 = @{thm le_maxI1}
+val le_maxI2 = @{thm le_maxI2}
+val less_max_iff_disj = @{thm less_max_iff_disj}
+val max_less_iff_conj = @{thm max_less_iff_conj}
+val min_less_iff_conj = @{thm min_less_iff_conj}
+val min_le_iff_disj = @{thm min_le_iff_disj}
+val min_less_iff_disj = @{thm min_less_iff_disj}
+val split_min = @{thm split_min}
+val split_max = @{thm split_max}
*}
end
--- a/src/HOL/Set.thy Sat Jan 20 14:09:23 2007 +0100
+++ b/src/HOL/Set.thy Sat Jan 20 14:09:27 2007 +0100
@@ -391,7 +391,8 @@
lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
by (unfold Ball_def) blast
-ML {* bind_thm("rev_ballE",permute_prems 1 1 (thm "ballE")) *}
+
+ML {* bind_thm ("rev_ballE", permute_prems 1 1 @{thm ballE}) *}
text {*
\medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and
@@ -399,8 +400,7 @@
*}
ML {*
- local val ballE = thm "ballE"
- in fun ball_tac i = etac ballE i THEN contr_tac (i + 1) end;
+ fun ball_tac i = etac @{thm ballE} i THEN contr_tac (i + 1)
*}
text {*
@@ -408,7 +408,7 @@
*}
ML_setup {*
- change_claset (fn cs => cs addbefore ("bspec", datac (thm "bspec") 1));
+ change_claset (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1))
*}
lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
@@ -454,11 +454,11 @@
ML_setup {*
local
- val unfold_bex_tac = unfold_tac [thm "Bex_def"];
+ val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
- val unfold_ball_tac = unfold_tac [thm "Ball_def"];
+ val unfold_ball_tac = unfold_tac @{thms "Ball_def"};
fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
in
@@ -524,8 +524,7 @@
*}
ML {*
- local val rev_subsetD = thm "rev_subsetD"
- in fun impOfSubs th = th RSN (2, rev_subsetD) end;
+ fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
*}
lemma subsetCE [elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
@@ -538,8 +537,7 @@
*}
ML {*
- local val subsetCE = thm "subsetCE"
- in fun set_mp_tac i = etac subsetCE i THEN mp_tac i end;
+ fun set_mp_tac i = etac @{thm subsetCE} i THEN mp_tac i
*}
lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
@@ -990,7 +988,7 @@
*)
ML_setup {*
- val mksimps_pairs = [("Ball", [thm "bspec"])] @ mksimps_pairs;
+ val mksimps_pairs = [("Ball", @{thms bspec})] @ mksimps_pairs;
change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs));
*}
@@ -2121,61 +2119,61 @@
subsection {* Basic ML bindings *}
ML {*
-val Ball_def = thm "Ball_def";
-val Bex_def = thm "Bex_def";
-val CollectD = thm "CollectD";
-val CollectE = thm "CollectE";
-val CollectI = thm "CollectI";
-val Collect_conj_eq = thm "Collect_conj_eq";
-val Collect_mem_eq = thm "Collect_mem_eq";
-val IntD1 = thm "IntD1";
-val IntD2 = thm "IntD2";
-val IntE = thm "IntE";
-val IntI = thm "IntI";
-val Int_Collect = thm "Int_Collect";
-val UNIV_I = thm "UNIV_I";
-val UNIV_witness = thm "UNIV_witness";
-val UnE = thm "UnE";
-val UnI1 = thm "UnI1";
-val UnI2 = thm "UnI2";
-val ballE = thm "ballE";
-val ballI = thm "ballI";
-val bexCI = thm "bexCI";
-val bexE = thm "bexE";
-val bexI = thm "bexI";
-val bex_triv = thm "bex_triv";
-val bspec = thm "bspec";
-val contra_subsetD = thm "contra_subsetD";
-val distinct_lemma = thm "distinct_lemma";
-val eq_to_mono = thm "eq_to_mono";
-val eq_to_mono2 = thm "eq_to_mono2";
-val equalityCE = thm "equalityCE";
-val equalityD1 = thm "equalityD1";
-val equalityD2 = thm "equalityD2";
-val equalityE = thm "equalityE";
-val equalityI = thm "equalityI";
-val imageE = thm "imageE";
-val imageI = thm "imageI";
-val image_Un = thm "image_Un";
-val image_insert = thm "image_insert";
-val insert_commute = thm "insert_commute";
-val insert_iff = thm "insert_iff";
-val mem_Collect_eq = thm "mem_Collect_eq";
-val rangeE = thm "rangeE";
-val rangeI = thm "rangeI";
-val range_eqI = thm "range_eqI";
-val subsetCE = thm "subsetCE";
-val subsetD = thm "subsetD";
-val subsetI = thm "subsetI";
-val subset_refl = thm "subset_refl";
-val subset_trans = thm "subset_trans";
-val vimageD = thm "vimageD";
-val vimageE = thm "vimageE";
-val vimageI = thm "vimageI";
-val vimageI2 = thm "vimageI2";
-val vimage_Collect = thm "vimage_Collect";
-val vimage_Int = thm "vimage_Int";
-val vimage_Un = thm "vimage_Un";
+val Ball_def = @{thm Ball_def}
+val Bex_def = @{thm Bex_def}
+val CollectD = @{thm CollectD}
+val CollectE = @{thm CollectE}
+val CollectI = @{thm CollectI}
+val Collect_conj_eq = @{thm Collect_conj_eq}
+val Collect_mem_eq = @{thm Collect_mem_eq}
+val IntD1 = @{thm IntD1}
+val IntD2 = @{thm IntD2}
+val IntE = @{thm IntE}
+val IntI = @{thm IntI}
+val Int_Collect = @{thm Int_Collect}
+val UNIV_I = @{thm UNIV_I}
+val UNIV_witness = @{thm UNIV_witness}
+val UnE = @{thm UnE}
+val UnI1 = @{thm UnI1}
+val UnI2 = @{thm UnI2}
+val ballE = @{thm ballE}
+val ballI = @{thm ballI}
+val bexCI = @{thm bexCI}
+val bexE = @{thm bexE}
+val bexI = @{thm bexI}
+val bex_triv = @{thm bex_triv}
+val bspec = @{thm bspec}
+val contra_subsetD = @{thm contra_subsetD}
+val distinct_lemma = @{thm distinct_lemma}
+val eq_to_mono = @{thm eq_to_mono}
+val eq_to_mono2 = @{thm eq_to_mono2}
+val equalityCE = @{thm equalityCE}
+val equalityD1 = @{thm equalityD1}
+val equalityD2 = @{thm equalityD2}
+val equalityE = @{thm equalityE}
+val equalityI = @{thm equalityI}
+val imageE = @{thm imageE}
+val imageI = @{thm imageI}
+val image_Un = @{thm image_Un}
+val image_insert = @{thm image_insert}
+val insert_commute = @{thm insert_commute}
+val insert_iff = @{thm insert_iff}
+val mem_Collect_eq = @{thm mem_Collect_eq}
+val rangeE = @{thm rangeE}
+val rangeI = @{thm rangeI}
+val range_eqI = @{thm range_eqI}
+val subsetCE = @{thm subsetCE}
+val subsetD = @{thm subsetD}
+val subsetI = @{thm subsetI}
+val subset_refl = @{thm subset_refl}
+val subset_trans = @{thm subset_trans}
+val vimageD = @{thm vimageD}
+val vimageE = @{thm vimageE}
+val vimageI = @{thm vimageI}
+val vimageI2 = @{thm vimageI2}
+val vimage_Collect = @{thm vimage_Collect}
+val vimage_Int = @{thm vimage_Int}
+val vimage_Un = @{thm vimage_Un}
*}
end