--- a/src/FOL/FOL.thy Sun Nov 27 23:06:59 2011 +0100
+++ b/src/FOL/FOL.thy Sun Nov 27 23:10:19 2011 +0100
@@ -337,12 +337,12 @@
(*intuitionistic simprules only*)
val IFOL_ss =
FOL_basic_ss
- addsimps (@{thms meta_simps} @ @{thms IFOL_simps} @ @{thms int_ex_simps} @ @{thms int_all_simps})
+ addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps}
addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}]
|> Simplifier.add_cong @{thm imp_cong};
(*classical simprules too*)
-val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps});
+val FOL_ss = IFOL_ss addsimps @{thms cla_simps cla_ex_simps cla_all_simps};
*}
setup {* Simplifier.map_simpset_global (K FOL_ss) *}
--- a/src/HOL/Decision_Procs/cooper_tac.ML Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Sun Nov 27 23:10:19 2011 +0100
@@ -19,7 +19,7 @@
val nT = HOLogic.natT;
val binarith = @{thms normalize_bin_simps};
-val comp_arith = binarith @ simp_thms
+val comp_arith = binarith @ @{thms simp_thms};
val zdvd_int = @{thm zdvd_int};
val zdiff_int_split = @{thm zdiff_int_split};
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Sun Nov 27 23:10:19 2011 +0100
@@ -23,7 +23,7 @@
val binarith =
@{thms normalize_bin_simps} @ @{thms pred_bin_simps} @ @{thms succ_bin_simps} @
@{thms add_bin_simps} @ @{thms minus_bin_simps} @ @{thms mult_bin_simps};
-val comp_arith = binarith @ simp_thms
+val comp_arith = binarith @ @{thms simp_thms};
val zdvd_int = @{thm zdvd_int};
val zdiff_int_split = @{thm zdiff_int_split};
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Sun Nov 27 23:10:19 2011 +0100
@@ -163,7 +163,7 @@
qe))
[fU, ld_th, nmi_th, npi_th, minf_th, pinf_th]
val bex_conv =
- Simplifier.rewrite (HOL_basic_ss addsimps simp_thms@(@{thms "bex_simps" (1-5)}))
+ Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms bex_simps(1-5)})
val result_th = fconv_rule (arg_conv bex_conv) (Thm.transitive enth qe_th)
in result_th
end
@@ -200,8 +200,8 @@
let
val ss = simpset
val ss' =
- merge_ss (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps)
- @ [not_all,@{thm "all_not_ex"}, ex_disj_distrib], ss)
+ merge_ss (HOL_basic_ss addsimps @{thms simp_thms ex_simps all_simps
+ not_all all_not_ex ex_disj_distrib}, ss)
|> Simplifier.inherit_context ss
val pcv = Simplifier.rewrite ss'
val postcv = Simplifier.rewrite ss
--- a/src/HOL/Decision_Procs/langford.ML Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Decision_Procs/langford.ML Sun Nov 27 23:10:19 2011 +0100
@@ -26,7 +26,9 @@
(Thm.cprop_of th), SOME x] th1) th
in fold ins u th0 end;
-val simp_rule = Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (HOL_basic_ss addsimps (@{thms "ball_simps"} @ simp_thms))));
+val simp_rule =
+ Conv.fconv_rule
+ (Conv.arg_conv (Simplifier.rewrite (HOL_basic_ss addsimps @{thms ball_simps simp_thms})));
fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep =
case term_of ep of
@@ -138,16 +140,14 @@
(Thm.capply @{cterm Trueprop} (list_conj (ndx @dx))))
|> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
|> Conv.fconv_rule (Conv.arg_conv
- (Simplifier.rewrite
- (HOL_basic_ss addsimps (simp_thms @ ex_simps))))
+ (Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms ex_simps})))
|> SOME
end
| _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp
(Thm.capply @{cterm Trueprop} (list_conj (eqs@neqs))))
|> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
|> Conv.fconv_rule (Conv.arg_conv
- (Simplifier.rewrite
- (HOL_basic_ss addsimps (simp_thms @ ex_simps))))
+ (Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms ex_simps})))
|> SOME
end
| _ => NONE;
@@ -162,9 +162,9 @@
let
val ss = dlo_ss addsimps @{thms "dnf_simps"} addsimprocs [reduce_ex_simproc]
val dnfex_conv = Simplifier.rewrite ss
- val pcv = Simplifier.rewrite
- (dlo_ss addsimps (simp_thms @ ex_simps @ all_simps)
- @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib])
+ val pcv =
+ Simplifier.rewrite
+ (dlo_ss addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib})
in fn p =>
Qelim.gen_qelim_conv pcv pcv dnfex_conv cons
(Thm.add_cterm_frees p []) (K Thm.reflexive) (K Thm.reflexive)
--- a/src/HOL/Decision_Procs/mir_tac.ML Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Sun Nov 27 23:10:19 2011 +0100
@@ -37,7 +37,7 @@
@{thm "divide_divide_eq_left"}, @{thm "times_divide_eq_right"},
@{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
@{thm "diff_minus"}, @{thm "minus_divide_left"}]
-val comp_ths = ths @ comp_arith @ simp_thms
+val comp_ths = ths @ comp_arith @ @{thms simp_thms};
val zdvd_int = @{thm "zdvd_int"};
@@ -89,7 +89,7 @@
fun mir_tac ctxt q =
Object_Logic.atomize_prems_tac
- THEN' simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms)
+ THEN' simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps @{thms simp_thms})
THEN' (REPEAT_DETERM o split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
THEN' SUBGOAL (fn (g, i) =>
let
--- a/src/HOL/HOL.thy Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/HOL.thy Sun Nov 27 23:10:19 2011 +0100
@@ -2011,15 +2011,8 @@
fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
end;
-val all_conj_distrib = @{thm all_conj_distrib};
-val all_simps = @{thms all_simps};
-val atomize_not = @{thm atomize_not};
val case_split = @{thm case_split};
-val cases_simp = @{thm cases_simp};
-val choice_eq = @{thm choice_eq};
val cong = @{thm cong};
-val conj_comms = @{thms conj_comms};
-val conj_cong = @{thm conj_cong};
val de_Morgan_conj = @{thm de_Morgan_conj};
val de_Morgan_disj = @{thm de_Morgan_disj};
val disj_assoc = @{thm disj_assoc};
@@ -2045,15 +2038,11 @@
val imp_conjL = @{thm imp_conjL};
val imp_conjR = @{thm imp_conjR};
val imp_conv_disj = @{thm imp_conv_disj};
-val simp_implies_def = @{thm simp_implies_def};
-val simp_thms = @{thms simp_thms};
val split_if = @{thm split_if};
val the1_equality = @{thm the1_equality};
val theI = @{thm theI};
val theI' = @{thm theI'};
-val True_implies_equals = @{thm True_implies_equals};
-val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms @ @{thms "nnf_simps"})
-
+val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms nnf_simps});
*}
hide_const (open) eq equal
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sun Nov 27 23:10:19 2011 +0100
@@ -64,13 +64,13 @@
(************************** miscellaneous functions ***************************)
-val simple_ss = HOL_basic_ss addsimps simp_thms
+val simple_ss = HOL_basic_ss addsimps @{thms simp_thms}
val beta_rules =
@{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
@{thms cont2cont_fst cont2cont_snd cont2cont_Pair}
-val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules)
+val beta_ss = HOL_basic_ss addsimps (@{thms simp_thms} @ beta_rules)
fun define_consts
(specs : (binding * term * mixfix) list)
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sun Nov 27 23:10:19 2011 +0100
@@ -156,7 +156,7 @@
fun con_thm p (con, args) =
let
val subgoal = con_assm false p (con, args)
- val rules = prems @ con_rews @ simp_thms
+ val rules = prems @ con_rews @ @{thms simp_thms}
val simplify = asm_simp_tac (HOL_basic_ss addsimps rules)
fun arg_tac (lazy, _) =
rtac (if lazy then allI else case_UU_allI) 1
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Nov 27 23:10:19 2011 +0100
@@ -36,7 +36,7 @@
struct
val beta_ss =
- HOL_basic_ss addsimps simp_thms addsimprocs [@{simproc beta_cfun_proc}]
+ HOL_basic_ss addsimps @{thms simp_thms} addsimprocs [@{simproc beta_cfun_proc}]
fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo})
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Sun Nov 27 23:10:19 2011 +0100
@@ -108,7 +108,7 @@
}
val beta_ss =
- HOL_basic_ss addsimps simp_thms addsimprocs [@{simproc beta_cfun_proc}]
+ HOL_basic_ss addsimps @{thms simp_thms} addsimprocs [@{simproc beta_cfun_proc}]
(******************************************************************************)
(******************************** theory data *********************************)
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Sun Nov 27 23:10:19 2011 +0100
@@ -381,7 +381,7 @@
@{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
@{thms cont2cont_fst cont2cont_snd cont2cont_Pair};
-val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
+val beta_ss = HOL_basic_ss addsimps (@{thms simp_thms} @ beta_rules);
fun define_consts
(specs : (binding * term * mixfix) list)
--- a/src/HOL/Library/positivstellensatz.ML Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Library/positivstellensatz.ML Sun Nov 27 23:10:19 2011 +0100
@@ -200,7 +200,7 @@
val pth_square = @{lemma "x * x >= (0::real)" by simp};
val weak_dnf_simps =
- List.take (simp_thms, 34) @
+ List.take (@{thms simp_thms}, 34) @
@{lemma "((P & (Q | R)) = ((P&Q) | (P&R)))" and "((Q | R) & P) = ((Q&P) | (R&P))" and
"(P & Q) = (Q & P)" and "((P | Q) = (Q | P))" by blast+};
@@ -351,7 +351,8 @@
poly_conv,poly_neg_conv,poly_add_conv,poly_mul_conv,
absconv1,absconv2,prover) =
let
- val pre_ss = HOL_basic_ss addsimps simp_thms@ ex_simps@ all_simps@[@{thm not_all},@{thm not_ex},ex_disj_distrib, all_conj_distrib, @{thm if_bool_eq_disj}]
+ val pre_ss = HOL_basic_ss addsimps
+ @{thms simp_thms ex_simps all_simps not_all not_ex ex_disj_distrib all_conj_distrib if_bool_eq_disj}
val prenex_ss = HOL_basic_ss addsimps prenex_simps
val skolemize_ss = HOL_basic_ss addsimps [choice_iff]
val presimp_conv = Simplifier.rewrite (Simplifier.context ctxt pre_ss)
--- a/src/HOL/Nominal/nominal_datatype.ML Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Sun Nov 27 23:10:19 2011 +0100
@@ -1018,7 +1018,7 @@
(fn _ =>
simp_tac (HOL_basic_ss addsimps (supp_def ::
Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
- Collect_False_empty :: finite_emptyI :: simp_thms @
+ Collect_False_empty :: finite_emptyI :: @{thms simp_thms} @
abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
in
(supp_thm,
--- a/src/HOL/Prolog/prolog.ML Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Prolog/prolog.ML Sun Nov 27 23:10:19 2011 +0100
@@ -62,7 +62,7 @@
(Simplifier.global_context @{theory} empty_ss
|> Simplifier.set_mksimps (mksimps mksimps_pairs))
addsimps [
- all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
+ @{thm all_conj_distrib}, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
imp_conjR, (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
imp_all]; (* "((!x. D) :- G) = (!x. D :- G)" *)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Sun Nov 27 23:10:19 2011 +0100
@@ -38,7 +38,7 @@
(** special setup for simpset **)
-val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms HOL.simp_thms} @ [@{thm Pair_eq}])
+val HOL_basic_ss' = HOL_basic_ss addsimps @{thms simp_thms Pair_eq}
setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))
@@ -206,7 +206,7 @@
preds
in
simp_tac (HOL_basic_ss addsimps
- (@{thms HOL.simp_thms} @ (@{thm eval_pred} :: defs))) 1
+ (@{thms HOL.simp_thms eval_pred} @ defs)) 1
(* need better control here! *)
end
--- a/src/HOL/Tools/Qelim/qelim.ML Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Tools/Qelim/qelim.ML Sun Nov 27 23:10:19 2011 +0100
@@ -55,8 +55,7 @@
local
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}]));
+ (HOL_basic_ss addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all 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