--- a/src/HOL/Groebner_Basis.thy Sun Feb 28 22:30:51 2010 +0100
+++ b/src/HOL/Groebner_Basis.thy Sun Feb 28 23:51:31 2010 +0100
@@ -510,7 +510,7 @@
let
val z = instantiate_cterm ([(zT,T)],[]) zr
val eq = instantiate_cterm ([(eqT,T)],[]) geq
- val th = Simplifier.rewrite (ss addsimps simp_thms)
+ val th = Simplifier.rewrite (ss addsimps @{thms simp_thms})
(Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"}
(Thm.capply (Thm.capply eq t) z)))
in equal_elim (symmetric th) TrueI
@@ -640,7 +640,7 @@
val comp_conv = (Simplifier.rewrite
(HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
- addsimps ths addsimps simp_thms
+ addsimps ths addsimps @{thms simp_thms}
addsimprocs Numeral_Simprocs.field_cancel_numeral_factors
addsimprocs [add_frac_frac_simproc, add_frac_num_simproc,
ord_frac_simproc]
--- a/src/HOL/Statespace/state_fun.ML Sun Feb 28 22:30:51 2010 +0100
+++ b/src/HOL/Statespace/state_fun.ML Sun Feb 28 23:51:31 2010 +0100
@@ -76,7 +76,7 @@
val string_eq_simp_tac = simp_tac (HOL_basic_ss
addsimps (@{thms list.inject} @ @{thms char.inject}
- @ @{thms list.distinct} @ @{thms char.distinct} @ simp_thms)
+ @ @{thms list.distinct} @ @{thms char.distinct} @ @{thms simp_thms})
addsimprocs [lazy_conj_simproc]
addcongs [@{thm block_conj_cong}])
@@ -84,7 +84,7 @@
val lookup_ss = (HOL_basic_ss
addsimps (@{thms list.inject} @ @{thms char.inject}
- @ @{thms list.distinct} @ @{thms char.distinct} @ simp_thms
+ @ @{thms list.distinct} @ @{thms char.distinct} @ @{thms simp_thms}
@ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel},
@{thm StateFun.lookup_update_same}, @{thm StateFun.lookup_update_other}])
addsimprocs [lazy_conj_simproc]
--- a/src/HOL/Tools/Datatype/datatype.ML Sun Feb 28 22:30:51 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Sun Feb 28 23:51:31 2010 +0100
@@ -481,7 +481,7 @@
(Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
[(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
REPEAT (rtac TrueI 1),
- rewrite_goals_tac (mk_meta_eq choice_eq ::
+ rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs),
rewrite_goals_tac (map symmetric range_eqs),
REPEAT (EVERY
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Sun Feb 28 22:30:51 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Sun Feb 28 23:51:31 2010 +0100
@@ -210,13 +210,13 @@
(map cert insts)) induct;
val (tac, _) = fold mk_unique_tac (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
(((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
- THEN rewrite_goals_tac [mk_meta_eq choice_eq], rec_intrs));
+ THEN rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs));
in split_conj_thm (Skip_Proof.prove_global thy1 [] []
(HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))
end;
- val rec_total_thms = map (fn r => r RS theI') rec_unique_thms;
+ val rec_total_thms = map (fn r => r RS @{thm theI'}) rec_unique_thms;
(* define primrec combinators *)
@@ -250,7 +250,7 @@
val rec_thms = map (fn t => Skip_Proof.prove_global thy2 [] [] t
(fn _ => EVERY
[rewrite_goals_tac reccomb_defs,
- rtac the1_equality 1,
+ rtac @{thm the1_equality} 1,
resolve_tac rec_unique_thms 1,
resolve_tac rec_intrs 1,
REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
--- a/src/HOL/Tools/Function/function.ML Sun Feb 28 22:30:51 2010 +0100
+++ b/src/HOL/Tools/Function/function.ML Sun Feb 28 23:51:31 2010 +0100
@@ -146,7 +146,7 @@
let
val totality = Thm.close_derivation totality
val remove_domain_condition =
- full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
+ full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}])
val tsimps = map remove_domain_condition psimps
val tinduct = map remove_domain_condition pinducts
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML Sun Feb 28 22:30:51 2010 +0100
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Sun Feb 28 23:51:31 2010 +0100
@@ -447,7 +447,8 @@
val initial_conv =
Simplifier.rewrite
(HOL_basic_ss addsimps nnf_simps
- addsimps [not_all, not_ex] addsimps map (fn th => th RS sym) (ex_simps @ all_simps));
+ addsimps [not_all, not_ex]
+ addsimps map (fn th => th RS sym) (@{thms ex_simps} @ @{thms all_simps}));
val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
@@ -820,7 +821,7 @@
in make_simproc {lhss = [Thm.lhs_of idl_sub],
name = "poly_eq_simproc", proc = proc, identifier = []}
end;
- val poly_eq_ss = HOL_basic_ss addsimps simp_thms
+ val poly_eq_ss = HOL_basic_ss addsimps @{thms simp_thms}
addsimprocs [poly_eq_simproc]
local
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Sun Feb 28 22:30:51 2010 +0100
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Sun Feb 28 23:51:31 2010 +0100
@@ -60,7 +60,7 @@
(Simplifier.rewrite
(HOL_basic_ss
addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps}
- @ [if_False, if_True, @{thm Nat.add_0}, @{thm add_Suc},
+ @ [@{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc},
@{thm add_number_of_left}, @{thm Suc_eq_plus1}]
@ map (fn th => th RS sym) @{thms numerals}));
@@ -632,9 +632,9 @@
end
end;
-val nat_arith = @{thms "nat_arith"};
-val nat_exp_ss = HOL_basic_ss addsimps (@{thms nat_number} @ nat_arith @ @{thms arith_simps} @ @{thms rel_simps})
- addsimps [Let_def, if_False, if_True, @{thm Nat.add_0}, @{thm add_Suc}];
+val nat_exp_ss =
+ HOL_basic_ss addsimps (@{thms nat_number} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps})
+ addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}];
fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;
--- a/src/HOL/Tools/Qelim/cooper.ML Sun Feb 28 22:30:51 2010 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Sun Feb 28 23:51:31 2010 +0100
@@ -16,7 +16,7 @@
exception COOPER of string * exn;
fun simp_thms_conv ctxt =
- Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps simp_thms);
+ Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps @{thms simp_thms});
val FWD = Drule.implies_elim_list;
val true_tm = @{cterm "True"};
@@ -514,8 +514,8 @@
local
val pcv = Simplifier.rewrite
- (HOL_basic_ss addsimps (simp_thms @ (List.take(ex_simps,4))
- @ [not_all,all_not_ex, ex_disj_distrib]))
+ (HOL_basic_ss addsimps (@{thms simp_thms} @ List.take(@{thms ex_simps}, 4)
+ @ [not_all, all_not_ex, @{thm ex_disj_distrib}]))
val postcv = Simplifier.rewrite presburger_ss
fun conv ctxt p =
let val _ = ()
--- a/src/HOL/Tools/Qelim/presburger.ML Sun Feb 28 22:30:51 2010 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML Sun Feb 28 23:51:31 2010 +0100
@@ -109,7 +109,7 @@
local
val ss1 = comp_ss
- addsimps simp_thms @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}]
+ addsimps @{thms simp_thms} @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}]
@ map (fn r => r RS sym)
[@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"},
@{thm "zmult_int"}]
@@ -120,7 +120,7 @@
@{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"},
@{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
-val div_mod_ss = HOL_basic_ss addsimps simp_thms
+val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms}
@ map (symmetric o mk_meta_eq)
[@{thm "dvd_eq_mod_eq_0"},
@{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"},
--- a/src/HOL/Tools/Qelim/qelim.ML Sun Feb 28 22:30:51 2010 +0100
+++ b/src/HOL/Tools/Qelim/qelim.ML Sun Feb 28 23:51:31 2010 +0100
@@ -55,9 +55,10 @@
(* Instantiation of some parameter for most common cases *)
local
-val pcv = Simplifier.rewrite
- (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps)
- @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib]);
+val pcv =
+ Simplifier.rewrite
+ (HOL_basic_ss addsimps (@{thms simp_thms} @ @{thms ex_simps} @ @{thms all_simps} @
+ [@{thm all_not_ex}, not_all, @{thm ex_disj_distrib}]));
in fun standard_qelim_conv atcv ncv qcv p =
gen_qelim_conv pcv pcv pcv cons (Thm.add_cterm_frees p []) atcv ncv qcv p
--- a/src/HOL/Tools/arith_data.ML Sun Feb 28 22:30:51 2010 +0100
+++ b/src/HOL/Tools/arith_data.ML Sun Feb 28 23:51:31 2010 +0100
@@ -120,7 +120,7 @@
in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
fun simplify_meta_eq rules =
- let val ss0 = HOL_basic_ss addeqcongs [eq_cong2] addsimps rules
+ let val ss0 = HOL_basic_ss addeqcongs [@{thm eq_cong2}] addsimps rules
in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end
fun trans_tac NONE = all_tac
--- a/src/HOL/Tools/lin_arith.ML Sun Feb 28 22:30:51 2010 +0100
+++ b/src/HOL/Tools/lin_arith.ML Sun Feb 28 23:51:31 2010 +0100
@@ -42,7 +42,7 @@
val not_lessD = @{thm linorder_not_less} RS iffD1;
val not_leD = @{thm linorder_not_le} RS iffD1;
-fun mk_Eq thm = thm RS Eq_FalseI handle THM _ => thm RS Eq_TrueI;
+fun mk_Eq thm = thm RS @{thm Eq_FalseI} handle THM _ => thm RS @{thm Eq_TrueI};
val mk_Trueprop = HOLogic.mk_Trueprop;
@@ -703,8 +703,8 @@
val nnf_simpset =
empty_ss setmkeqTrue mk_eq_True
setmksimps (mksimps mksimps_pairs)
- addsimps [imp_conv_disj, iff_conv_conj_imp, de_Morgan_disj, de_Morgan_conj,
- not_all, not_ex, not_not]
+ addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
+ @{thm de_Morgan_conj}, not_all, not_ex, not_not]
fun prem_nnf_tac ss = full_simp_tac (Simplifier.inherit_context ss nnf_simpset)
in
@@ -823,7 +823,7 @@
addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
(*abel_cancel helps it work in abstract algebraic domains*)
addsimprocs Nat_Arith.nat_cancel_sums_add
- addcongs [if_weak_cong],
+ addcongs [@{thm if_weak_cong}],
number_of = number_of}) #>
add_discrete_type @{type_name nat};
--- a/src/HOL/Tools/meson.ML Sun Feb 28 22:30:51 2010 +0100
+++ b/src/HOL/Tools/meson.ML Sun Feb 28 23:51:31 2010 +0100
@@ -517,10 +517,10 @@
nnf_ss also includes the one-point simprocs,
which are needed to avoid the various one-point theorems from generating junk clauses.*)
val nnf_simps =
- [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True,
- if_False, if_cancel, if_eq_cancel, cases_simp];
+ [@{thm simp_implies_def}, @{thm Ex1_def}, @{thm Ball_def},@{thm Bex_def}, @{thm if_True},
+ @{thm if_False}, @{thm if_cancel}, @{thm if_eq_cancel}, @{thm cases_simp}];
val nnf_extra_simps =
- thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
+ @{thms split_ifs} @ @{thms ex_simps} @ @{thms all_simps} @ @{thms simp_thms};
val nnf_ss =
HOL_basic_ss addsimps nnf_extra_simps
@@ -685,7 +685,7 @@
(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
double-negations.*)
-val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
+val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection];
(*Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
fun select_literal i cl = negate_head (make_last i cl);
--- a/src/HOL/Tools/record.ML Sun Feb 28 22:30:51 2010 +0100
+++ b/src/HOL/Tools/record.ML Sun Feb 28 23:51:31 2010 +0100
@@ -1416,7 +1416,7 @@
| name =>
(case get_equalities thy name of
NONE => NONE
- | SOME thm => SOME (thm RS Eq_TrueI)))
+ | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
| _ => NONE));
@@ -1462,7 +1462,7 @@
fun prove prop =
prove_global true thy [] prop
(fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
- addsimps simp_thms addsimprocs [record_split_simproc (K ~1)]) 1);
+ addsimps @{thms simp_thms} addsimprocs [record_split_simproc (K ~1)]) 1);
fun mkeq (lr, Teq, (sel, Tsel), x) i =
if is_selector thy sel then