--- a/src/CCL/CCL.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/CCL/CCL.thy Wed Mar 19 22:50:42 2008 +0100
@@ -390,7 +390,7 @@
local
fun mk_thm s = prove_goal (the_context ()) s (fn _ =>
[rtac notI 1,dtac (thm "case_pocong") 1,etac rev_mp 5,
- ALLGOALS (simp_tac (simpset ())),
+ ALLGOALS (simp_tac @{simpset}),
REPEAT (resolve_tac [thm "po_refl", thm "npo_lam_bot"] 1)])
in
--- a/src/CCL/Term.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/CCL/Term.thy Wed Mar 19 22:50:42 2008 +0100
@@ -209,11 +209,11 @@
fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s
(fn _ => [stac letrecB 1,
- simp_tac (simpset () addsimps rawBs) 1]);
+ simp_tac (@{simpset} addsimps rawBs) 1]);
fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s
- (fn _ => [simp_tac (simpset () addsimps rawBs
+ (fn _ => [simp_tac (@{simpset} addsimps rawBs
setloop (stac letrecB)) 1]);
fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
@@ -298,7 +298,7 @@
local
fun mk_thm s = prove_goalw (the_context ()) (thms "data_defs") s (fn _ =>
- [simp_tac (simpset () addsimps (thms "ccl_porews")) 1])
+ [simp_tac (@{simpset} addsimps (thms "ccl_porews")) 1])
in
val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
"inr(b) [= inr(b') <-> b [= b'",
--- a/src/CCL/Type.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/CCL/Type.thy Wed Mar 19 22:50:42 2008 +0100
@@ -397,7 +397,7 @@
val lfpI = thm "lfpI"
val coinduct3_mono_lemma = thm "coinduct3_mono_lemma"
fun mk_thm s = prove_goal (the_context ()) s (fn mono::prems =>
- [fast_tac (claset () addIs ((mono RS coinduct3_mono_lemma RS lfpI)::prems)) 1])
+ [fast_tac (@{claset} addIs ((mono RS coinduct3_mono_lemma RS lfpI)::prems)) 1])
in
val ci3_RI = mk_thm "[| mono(Agen); a : R |] ==> a : lfp(%x. Agen(x) Un R Un A)"
val ci3_AgenI = mk_thm "[| mono(Agen); a : Agen(lfp(%x. Agen(x) Un R Un A)) |] ==> a : lfp(%x. Agen(x) Un R Un A)"
@@ -405,8 +405,8 @@
fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s
(fn prems => [rtac (genXH RS iffD2) 1,
- simp_tac (simpset ()) 1,
- TRY (fast_tac (claset () addIs
+ SIMPSET' simp_tac 1,
+ TRY (fast_tac (@{claset} addIs
([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI]
@ prems)) 1)])
end;
--- a/src/FOL/ex/Classical.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/FOL/ex/Classical.thy Wed Mar 19 22:50:42 2008 +0100
@@ -459,7 +459,7 @@
((C(y) & Q(w,y,y)) & OO(w,b) --> P(v,y) & OO(v,b)))))
-->
~ (\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z))))"
-by (tactic{*Blast.depth_tac (claset ()) 12 1*})
+by (tactic{*Blast.depth_tac @{claset} 12 1*})
--{*Needed because the search for depths below 12 is very slow*}
--- a/src/FOL/ex/Miniscope.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/FOL/ex/Miniscope.thy Wed Mar 19 22:50:42 2008 +0100
@@ -65,8 +65,8 @@
lemmas mini_simps = demorgans nnf_simps ex_simps all_simps
ML {*
-val mini_ss = simpset() addsimps (thms "mini_simps");
-val mini_tac = rtac (thm "ccontr") THEN' asm_full_simp_tac mini_ss;
+val mini_ss = @{simpset} addsimps @{thms mini_simps};
+val mini_tac = rtac @{thm ccontr} THEN' asm_full_simp_tac mini_ss;
*}
end
--- a/src/HOL/Algebra/abstract/Ideal2.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Algebra/abstract/Ideal2.thy Wed Mar 19 22:50:42 2008 +0100
@@ -115,8 +115,8 @@
apply (rule subsetI)
apply (drule InterD)
prefer 2 apply assumption
- apply (tactic {* auto_tac (claset() addIs [thm "is_ideal_2"],
- simpset() delsimprocs [ring_simproc]) *})
+ apply (tactic {* auto_tac (@{claset} addIs [@{thm is_ideal_2}],
+ @{simpset} delsimprocs [ring_simproc]) *})
apply (rule_tac x = "1" in exI)
apply (rule_tac x = "0" in exI)
apply (rule_tac [2] x = "0" in exI)
@@ -283,7 +283,7 @@
apply (drule_tac f = "op* aa" in arg_cong)
apply (simp add: r_distr)
apply (erule subst)
- apply (tactic {* asm_simp_tac (simpset() addsimps [thm "m_assoc" RS sym]
+ apply (tactic {* asm_simp_tac (@{simpset} addsimps [@{thm m_assoc} RS sym]
delsimprocs [ring_simproc]) 1 *})
done
--- a/src/HOL/Algebra/abstract/Ring2.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy Wed Mar 19 22:50:42 2008 +0100
@@ -465,7 +465,7 @@
lemma r_inverse_ring: "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1"
apply (unfold inverse_def dvd_def)
- apply (tactic {* asm_full_simp_tac (simpset () delsimprocs [ring_simproc]) 1 *})
+ apply (tactic {* asm_full_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *})
apply clarify
apply (rule theI)
apply assumption
--- a/src/HOL/Algebra/poly/LongDiv.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Algebra/poly/LongDiv.thy Wed Mar 19 22:50:42 2008 +0100
@@ -129,16 +129,16 @@
apply (rule_tac x = "((% (q,r,k) . (monom (lcoeff g ^ k * lcoeff x) (deg x - deg g) + q)) xa, (% (q,r,k) . r) xa, (% (q,r,k) . Suc k) xa) " in exI)
apply clarify
apply (drule sym)
- apply (tactic {* simp_tac (simpset() addsimps [thm "l_distr", thm "a_assoc"]
+ apply (tactic {* simp_tac (@{simpset} addsimps [@{thm l_distr}, @{thm a_assoc}]
delsimprocs [ring_simproc]) 1 *})
- apply (tactic {* asm_simp_tac (simpset() delsimprocs [ring_simproc]) 1 *})
- apply (tactic {* simp_tac (simpset () addsimps [thm "minus_def", thm "smult_r_distr",
+ apply (tactic {* asm_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *})
+ apply (tactic {* simp_tac (@{simpset} addsimps [thm "minus_def", thm "smult_r_distr",
thm "smult_r_minus", thm "monom_mult_smult", thm "smult_assoc1", thm "smult_assoc2"]
delsimprocs [ring_simproc]) 1 *})
apply simp
done
-ML {* simplify (simpset() addsimps [thm "eucl_size_def"]
+ML {* simplify (@{simpset} addsimps [thm "eucl_size_def"]
delsimprocs [ring_simproc]) (thm "long_div_eucl_size") *}
thm long_div_eucl_size [simplified]
@@ -148,9 +148,9 @@
Ex (% (q, r, k).
(lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))"
apply (tactic {* forw_inst_tac [("f", "f")]
- (simplify (simpset() addsimps [thm "eucl_size_def"]
+ (simplify (@{simpset} addsimps [thm "eucl_size_def"]
delsimprocs [ring_simproc]) (thm "long_div_eucl_size")) 1 *})
- apply (tactic {* auto_tac (claset(), simpset() delsimprocs [ring_simproc]) *})
+ apply (tactic {* auto_tac (@{claset}, @{simpset} delsimprocs [ring_simproc]) *})
apply (case_tac "aa = 0")
apply blast
(* case "aa ~= 0 *)
@@ -169,7 +169,7 @@
apply (rule conjI)
apply (drule sym)
apply (tactic {* asm_simp_tac
- (simpset() addsimps [thm "smult_r_distr" RS sym, thm "smult_assoc2"]
+ (@{simpset} addsimps [thm "smult_r_distr" RS sym, thm "smult_assoc2"]
delsimprocs [ring_simproc]) 1 *})
apply (simp (no_asm_simp) add: l_inverse_ring unit_power smult_assoc1 [symmetric])
(* degree property *)
@@ -194,7 +194,7 @@
lemma diff_zero_imp_eq: "!!a::'a::ring. a - b = 0 ==> a = b"
apply (rule_tac s = "a - (a - b) " in trans)
- apply (tactic {* asm_simp_tac (simpset() delsimprocs [ring_simproc]) 1 *})
+ apply (tactic {* asm_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *})
apply simp
apply (simp (no_asm))
done
@@ -215,22 +215,22 @@
(* r1 = 0 *)
apply (erule disjE)
(* r2 = 0 *)
- apply (tactic {* asm_full_simp_tac (simpset()
+ apply (tactic {* asm_full_simp_tac (@{simpset}
addsimps [thm "integral_iff", thm "minus_def", thm "l_zero", thm "uminus_zero"]
delsimprocs [ring_simproc]) 1 *})
(* r2 ~= 0 *)
apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
- apply (tactic {* asm_full_simp_tac (simpset() addsimps
+ apply (tactic {* asm_full_simp_tac (@{simpset} addsimps
[thm "minus_def", thm "l_zero", thm "uminus_zero"] delsimprocs [ring_simproc]) 1 *})
(* r1 ~=0 *)
apply (erule disjE)
(* r2 = 0 *)
apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
- apply (tactic {* asm_full_simp_tac (simpset() addsimps
+ apply (tactic {* asm_full_simp_tac (@{simpset} addsimps
[thm "minus_def", thm "l_zero", thm "uminus_zero"] delsimprocs [ring_simproc]) 1 *})
(* r2 ~= 0 *)
apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
- apply (tactic {* asm_full_simp_tac (simpset() addsimps [thm "minus_def"]
+ apply (tactic {* asm_full_simp_tac (@{simpset} addsimps [thm "minus_def"]
delsimprocs [ring_simproc]) 1 *})
apply (drule order_eq_refl [THEN add_leD2])
apply (drule leD)
--- a/src/HOL/Auth/Message.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Auth/Message.thy Wed Mar 19 22:50:42 2008 +0100
@@ -847,8 +847,8 @@
concerns Crypt K X \<notin> Key`shrK`bad and cannot be proved by rewriting
alone.*)
fun prove_simple_subgoals_tac i =
- force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN
- ALLGOALS Asm_simp_tac
+ CLASIMPSET' (fn (cs, ss) => force_tac (cs, ss addsimps [@{thm image_eq_UN}])) i THEN
+ ALLGOALS (SIMPSET' asm_simp_tac)
(*Analysis of Fake cases. Also works for messages that forward unknown parts,
but this application is no longer necessary if analz_insert_eq is used.
@@ -886,7 +886,7 @@
REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
-fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
+val spy_analz_tac = CLASIMPSET' gen_spy_analz_tac;
end
*}
--- a/src/HOL/Bali/AxExample.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Bali/AxExample.thy Wed Mar 19 22:50:42 2008 +0100
@@ -136,7 +136,7 @@
apply (rule ax_subst_Var_allI)
apply (tactic {* inst1_tac "P'" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
apply (rule allI)
-apply (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *})
+apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *})
apply (rule ax_derivs.Abrupt)
apply (simp (no_asm))
apply (tactic "ax_tac 1" (* FVar *))
@@ -186,26 +186,26 @@
apply (rule ax_InitS)
apply force
apply (simp (no_asm))
-apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
+apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *})
apply (rule ax_Init_Skip_lemma)
-apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
+apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *})
apply (rule ax_InitS [THEN conseq1] (* init Base *))
apply force
apply (simp (no_asm))
apply (unfold arr_viewed_from_def)
apply (rule allI)
apply (rule_tac P' = "Normal ?P" in conseq1)
-apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
+apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *})
apply (tactic "ax_tac 1")
apply (tactic "ax_tac 1")
apply (rule_tac [2] ax_subst_Var_allI)
apply (tactic {* inst1_tac "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
-apply (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [split_paired_All, thm "peek_and_def2"]) 2 *})
+apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [split_paired_All, thm "peek_and_def2"]) 2 *})
apply (tactic "ax_tac 2" (* NewA *))
apply (tactic "ax_tac 3" (* ax_Alloc_Arr *))
apply (tactic "ax_tac 3")
apply (tactic {* inst1_tac "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *})
-apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 2 *})
+apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 2 *})
apply (tactic "ax_tac 2")
apply (tactic "ax_tac 1" (* FVar *))
apply (tactic "ax_tac 2" (* StatRef *))
@@ -216,7 +216,7 @@
apply (drule initedD)
apply (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def)
apply force
-apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
+apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *})
apply (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
apply (rule wf_tprg)
apply clarsimp
--- a/src/HOL/Bali/AxSem.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Bali/AxSem.thy Wed Mar 19 22:50:42 2008 +0100
@@ -699,7 +699,7 @@
(*42 subgoals*)
apply (tactic "ALLGOALS strip_tac")
apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"),
- etac disjE, fast_tac (claset() addSIs [thm "ax_derivs.empty"])]))*})
+ etac disjE, fast_tac (@{claset} addSIs [thm "ax_derivs.empty"])]))*})
apply (tactic "TRYALL hyp_subst_tac")
apply (simp, rule ax_derivs.empty)
apply (drule subset_insertD)
--- a/src/HOL/Bali/Example.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Bali/Example.thy Wed Mar 19 22:50:42 2008 +0100
@@ -1193,7 +1193,7 @@
Base_foo_defs [simp]
ML_setup {* bind_thms ("eval_intros", map
- (simplify (simpset() delsimps @{thms Skip_eq}
+ (simplify (@{simpset} delsimps @{thms Skip_eq}
addsimps @{thms lvar_def}) o
rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
--- a/src/HOL/Fun.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Fun.thy Wed Mar 19 22:50:42 2008 +0100
@@ -532,7 +532,7 @@
subsection {* ML legacy bindings *}
ML {*
-val set_cs = claset() delrules [equalityI]
+val set_cs = @{claset} delrules [@{thm equalityI}]
*}
ML {*
--- a/src/HOL/HoareParallel/Gar_Coll.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/HoareParallel/Gar_Coll.thy Wed Mar 19 22:50:42 2008 +0100
@@ -796,9 +796,9 @@
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
apply(tactic {* TRYALL (etac disjE) *})
apply simp_all
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac (thm "Graph3"),force_tac (clasimpset ()), assume_tac]) *})
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
-apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{clasimpset}, assume_tac]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{clasimpset}]) *})
done
subsubsection {* Interference freedom Mutator-Collector *}
--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy Wed Mar 19 22:50:42 2008 +0100
@@ -1200,7 +1200,7 @@
--{* 72 subgoals left *}
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
--{* 35 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac (thm "Graph3"),force_tac (clasimpset ()), assume_tac]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{clasimpset}, assume_tac]) *})
--{* 28 subgoals left *}
apply(tactic {* TRYALL (etac conjE) *})
apply(tactic {* TRYALL (etac disjE) *})
@@ -1210,17 +1210,17 @@
apply(tactic {* ALLGOALS(case_tac "M x!(T (Muts x ! j))=Black") *})
apply(simp_all add:Graph10)
--{* 47 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *})
+apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
--{* 41 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (claset(),simpset() addsimps [thm "Queue_def", @{thm less_Suc_eq_le}, thm "le_length_filter_update"])]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *})
--{* 35 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac @{clasimpset}]) *})
--{* 31 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
--{* 29 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *})
+apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
--{* 25 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (claset(),simpset() addsimps [thm "Queue_def", @{thm less_Suc_eq_le}, thm "le_length_filter_update"])]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *})
--{* 10 subgoals left *}
apply(rule disjI2,rule disjI2,rule conjI,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update, rule disjI1, rule less_imp_le, erule less_le_trans, force simp add:Queue_def less_Suc_eq_le le_length_filter_update)+
done
--- a/src/HOL/IMP/VC.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/IMP/VC.thy Wed Mar 19 22:50:42 2008 +0100
@@ -77,7 +77,7 @@
apply fast
(* if *)
apply atomize
- apply (tactic "Deepen_tac 4 1")
+ apply (tactic "deepen_tac @{claset} 4 1")
(* while *)
apply atomize
apply (intro allI impI)
--- a/src/HOL/IOA/Solve.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/IOA/Solve.thy Wed Mar 19 22:50:42 2008 +0100
@@ -149,7 +149,7 @@
apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: split_if)
apply (tactic {*
REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
- asm_full_simp_tac(simpset() addsimps[thm "comp1_reachable", thm "comp2_reachable"]) 1) *})
+ asm_full_simp_tac(@{simpset} addsimps[thm "comp1_reachable", thm "comp2_reachable"]) 1) *})
done
--- a/src/HOL/MicroJava/J/Conform.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy Wed Mar 19 22:50:42 2008 +0100
@@ -343,7 +343,7 @@
apply(rule hconfI)
apply(drule conforms_heapD)
apply(tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"]
- addDs [thm "hconfD"], simpset() delsimps [split_paired_All]) *})
+ addDs [thm "hconfD"], @{simpset} delsimps [split_paired_All]) *})
done
lemma conforms_upd_local:
--- a/src/HOL/Modelcheck/EindhovenSyn.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy Wed Mar 19 22:50:42 2008 +0100
@@ -72,7 +72,7 @@
(fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
val Eindhoven_ss =
- simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
+ @{simpset} addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
(*check if user has pmu installed*)
fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> "";
--- a/src/HOL/Modelcheck/MuckeSyn.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Modelcheck/MuckeSyn.thy Wed Mar 19 22:50:42 2008 +0100
@@ -221,7 +221,7 @@
Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
(fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
-val Mucke_ss = simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
+val Mucke_ss = @{simpset} addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
(* the interface *)
--- a/src/HOL/Modelcheck/mucke_oracle.ML Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Wed Mar 19 22:50:42 2008 +0100
@@ -111,7 +111,7 @@
(
OldGoals.push_proof();
OldGoals.goalw_cterm [] (cterm_of sign trm);
-by (simp_tac (simpset()) 1);
+by (SIMPSET' simp_tac 1);
let
val if_tmp_result = result()
in
--- a/src/HOL/NatBin.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/NatBin.thy Wed Mar 19 22:50:42 2008 +0100
@@ -625,7 +625,7 @@
ML
{*
-val numeral_ss = simpset() addsimps @{thms numerals};
+val numeral_ss = @{simpset} addsimps @{thms numerals};
val nat_bin_arith_setup =
LinArith.map_data
--- a/src/HOL/Nominal/Nominal.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Nominal/Nominal.thy Wed Mar 19 22:50:42 2008 +0100
@@ -386,9 +386,11 @@
and "a\<sharp>(x,y) \<Longrightarrow> a\<sharp>y"
by (simp_all add: fresh_prod)
-ML_setup {*
- val mksimps_pairs = ("Nominal.fresh", thms "fresh_prodD")::mksimps_pairs;
- change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs));
+ML {*
+ val mksimps_pairs = (@{const_name Nominal.fresh}, @{thms fresh_prodD}) :: mksimps_pairs;
+*}
+declaration {* fn _ =>
+ Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
*}
--- a/src/HOL/SET-Protocol/MessageSET.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/SET-Protocol/MessageSET.thy Wed Mar 19 22:50:42 2008 +0100
@@ -844,8 +844,8 @@
concerns Crypt K X \<notin> Key`shrK`bad and cannot be proved by rewriting
alone.*)
fun prove_simple_subgoals_tac i =
- force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN
- ALLGOALS Asm_simp_tac
+ CLASIMPSET' (fn (cs, ss) => force_tac (cs, ss addsimps [@{thm image_eq_UN}])) i THEN
+ ALLGOALS (SIMPSET' asm_simp_tac)
(*Analysis of Fake cases. Also works for messages that forward unknown parts,
but this application is no longer necessary if analz_insert_eq is used.
@@ -883,7 +883,7 @@
REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
-fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
+val spy_analz_tac = CLASIMPSET' gen_spy_analz_tac;
end
*}
--- a/src/HOL/TLA/Buffer/DBuffer.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/TLA/Buffer/DBuffer.thy Wed Mar 19 22:50:42 2008 +0100
@@ -63,7 +63,7 @@
apply (rule square_simulation)
apply clarsimp
apply (tactic
- {* action_simp_tac (simpset () addsimps (thm "hd_append" :: thms "db_defs")) [] [] 1 *})
+ {* action_simp_tac (@{simpset} addsimps (@{thm hd_append} :: @{thms db_defs})) [] [] 1 *})
done
--- a/src/HOL/TLA/Inc/Inc.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/TLA/Inc/Inc.thy Wed Mar 19 22:50:42 2008 +0100
@@ -115,7 +115,7 @@
by (auto simp: PsiInv_defs)
lemma PsiInv: "|- Psi --> []PsiInv"
- apply (tactic {* inv_tac (clasimpset () addsimps2 [thm "Psi_def"]) 1 *})
+ apply (tactic {* inv_tac (@{clasimpset} addsimps2 [@{thm Psi_def}]) 1 *})
apply (force simp: PsiInv_Init [try_rewrite] Init_def)
apply (auto intro: PsiInv_alpha1 [try_rewrite] PsiInv_alpha2 [try_rewrite]
PsiInv_beta1 [try_rewrite] PsiInv_beta2 [try_rewrite] PsiInv_gamma1 [try_rewrite]
@@ -128,7 +128,7 @@
*)
lemma "|- Psi --> []PsiInv"
- by (tactic {* auto_inv_tac (simpset() addsimps (thms "PsiInv_defs" @ thms "Psi_defs")) 1 *})
+ by (tactic {* auto_inv_tac (@{simpset} addsimps (@{thms PsiInv_defs} @ @{thms Psi_defs})) 1 *})
(**** Step simulation ****)
@@ -174,9 +174,9 @@
--> (pc1 = #g ~> pc1 = #a)"
apply (rule SF1)
apply (tactic
- {* action_simp_tac (simpset () addsimps (thms "Psi_defs")) [] [thm "squareE"] 1 *})
+ {* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
apply (tactic
- {* action_simp_tac (simpset () addsimps (thm "angle_def" :: thms "Psi_defs")) [] [] 1 *})
+ {* action_simp_tac (@{simpset} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
(* reduce |- []A --> <>Enabled B to |- A --> Enabled B *)
apply (auto intro!: InitDmd_gen [temp_use] N1_enabled_at_g [temp_use]
dest!: STL2_gen [temp_use] simp: Init_def)
@@ -195,8 +195,8 @@
"|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True
--> (pc2 = #g ~> pc2 = #a)"
apply (rule SF1)
- apply (tactic {* action_simp_tac (simpset () addsimps (thms "Psi_defs")) [] [thm "squareE"] 1 *})
- apply (tactic {* action_simp_tac (simpset () addsimps (thm "angle_def" :: thms "Psi_defs"))
+ apply (tactic {* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps @{thm angle_def} :: @{thms Psi_defs})
[] [] 1 *})
apply (auto intro!: InitDmd_gen [temp_use] N2_enabled_at_g [temp_use]
dest!: STL2_gen [temp_use] simp add: Init_def)
@@ -215,9 +215,9 @@
--> (pc2 = #b ~> pc2 = #g)"
apply (rule SF1)
apply (tactic
- {* action_simp_tac (simpset () addsimps (thms "Psi_defs")) [] [thm "squareE"] 1 *})
+ {* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
apply (tactic
- {* action_simp_tac (simpset () addsimps (thm "angle_def" :: thms "Psi_defs")) [] [] 1 *})
+ {* action_simp_tac (@{simpset} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
apply (auto intro!: InitDmd_gen [temp_use] N2_enabled_at_b [temp_use]
dest!: STL2_gen [temp_use] simp: Init_def)
done
@@ -257,9 +257,9 @@
& SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)
--> (pc1 = #a ~> pc1 = #b)"
apply (rule SF1)
- apply (tactic {* action_simp_tac (simpset () addsimps thms "Psi_defs") [] [thm "squareE"] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
apply (tactic
- {* action_simp_tac (simpset () addsimps (thm "angle_def" :: thms "Psi_defs")) [] [] 1 *})
+ {* action_simp_tac (@{simpset} addsimps (@{thm angle_def} :: @{thms Psi_defs})) [] [] 1 *})
apply (clarsimp intro!: N1_enabled_at_both_a [THEN DmdImpl [temp_use]])
apply (auto intro!: BoxDmd2_simple [temp_use] N2_live [temp_use]
simp: split_box_conj more_temp_simps)
--- a/src/HOL/TLA/Memory/MemClerk.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/TLA/Memory/MemClerk.thy Wed Mar 19 22:50:42 2008 +0100
@@ -84,7 +84,7 @@
lemma MClkFwd_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>
|- Calling send p & ~Calling rcv p & cst!p = #clkA
--> Enabled (MClkFwd send rcv cst p)"
- by (tactic {* action_simp_tac (simpset () addsimps [thm "MClkFwd_def",
+ by (tactic {* action_simp_tac (@{simpset} addsimps [thm "MClkFwd_def",
thm "Call_def", thm "caller_def", thm "rtrner_def"]) [exI]
[thm "base_enabled", Pair_inject] 1 *})
@@ -99,9 +99,9 @@
lemma MClkReply_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>
|- Calling send p & ~Calling rcv p & cst!p = #clkB
--> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
- apply (tactic {* action_simp_tac (simpset ())
+ apply (tactic {* action_simp_tac @{simpset}
[thm "MClkReply_change" RSN (2, thm "enabled_mono") ] [] 1 *})
- apply (tactic {* action_simp_tac (simpset () addsimps
+ apply (tactic {* action_simp_tac (@{simpset} addsimps
[thm "MClkReply_def", thm "Return_def", thm "caller_def", thm "rtrner_def"])
[exI] [thm "base_enabled", Pair_inject] 1 *})
done
--- a/src/HOL/TLA/Memory/Memory.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/TLA/Memory/Memory.thy Wed Mar 19 22:50:42 2008 +0100
@@ -152,7 +152,7 @@
(* The memory spec implies the memory invariant *)
lemma MemoryInvariant: "|- MSpec ch mm rs l --> [](MemInv mm l)"
by (tactic {* auto_inv_tac
- (simpset () addsimps (thms "RM_temp_defs" @ thms "RM_action_defs")) 1 *})
+ (@{simpset} addsimps (@{thms RM_temp_defs} @ @{thms RM_action_defs})) 1 *})
(* The invariant is trivial for non-locations *)
lemma NonMemLocInvariant: "|- #l ~: #MemLoc --> [](MemInv mm l)"
@@ -182,9 +182,9 @@
|- Calling ch p & (rs!p ~= #NotAResult)
--> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))"
apply (tactic
- {* action_simp_tac (simpset ()) [thm "MemReturn_change" RSN (2, thm "enabled_mono") ] [] 1 *})
+ {* action_simp_tac @{simpset} [thm "MemReturn_change" RSN (2, thm "enabled_mono") ] [] 1 *})
apply (tactic
- {* action_simp_tac (simpset () addsimps [thm "MemReturn_def", thm "Return_def",
+ {* action_simp_tac (@{simpset} addsimps [thm "MemReturn_def", thm "Return_def",
thm "rtrner_def"]) [exI] [thm "base_enabled", thm "Pair_inject"] 1 *})
done
@@ -228,11 +228,11 @@
--> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use])
apply (case_tac "arg (ch w p)")
- apply (tactic {* action_simp_tac (simpset () addsimps [thm "Read_def",
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "Read_def",
temp_rewrite (thm "enabled_ex")]) [thm "ReadInner_enabled", exI] [] 1 *})
apply (force dest: base_pair [temp_use])
apply (erule contrapos_np)
- apply (tactic {* action_simp_tac (simpset () addsimps [thm "Write_def",
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "Write_def",
temp_rewrite (thm "enabled_ex")])
[thm "WriteInner_enabled", exI] [] 1 *})
done
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Wed Mar 19 22:50:42 2008 +0100
@@ -220,9 +220,9 @@
apply (rule historyI)
apply assumption+
apply (rule MI_base)
- apply (tactic {* action_simp_tac (simpset () addsimps [thm "HInit_def"]) [] [] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "HInit_def"]) [] [] 1 *})
apply (erule fun_cong)
- apply (tactic {* action_simp_tac (simpset () addsimps [thm "HNext_def"])
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def"])
[thm "busy_squareI"] [] 1 *})
apply (erule fun_cong)
done
@@ -324,7 +324,7 @@
lemma S1Hist: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S1 rmhist p)
--> unchanged (rmhist!p)"
- by (tactic {* action_simp_tac (simpset () addsimps [thm "HNext_def", thm "S_def",
+ by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def", thm "S_def",
thm "S1_def", thm "MemReturn_def", thm "RPCFail_def", thm "MClkReply_def",
thm "Return_def"]) [] [temp_use (thm "squareE")] 1 *})
@@ -340,7 +340,7 @@
lemma S2Forward: "|- $(S2 rmhist p) & MClkFwd memCh crCh cst p
& unchanged (e p, r p, m p, rmhist!p)
--> (S3 rmhist p)$"
- by (tactic {* action_simp_tac (simpset () addsimps [thm "MClkFwd_def",
+ by (tactic {* action_simp_tac (@{simpset} addsimps [thm "MClkFwd_def",
thm "Call_def", thm "e_def", thm "r_def", thm "m_def", thm "caller_def",
thm "rtrner_def", thm "S_def", thm "S2_def", thm "S3_def", thm "Calling_def"]) [] [] 1 *})
@@ -376,7 +376,7 @@
lemma S3Forward: "|- RPCFwd crCh rmCh rst p & HNext rmhist p & $(S3 rmhist p)
& unchanged (e p, c p, m p)
--> (S4 rmhist p)$ & unchanged (rmhist!p)"
- by (tactic {* action_simp_tac (simpset () addsimps [thm "RPCFwd_def",
+ by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFwd_def",
thm "HNext_def", thm "MemReturn_def", thm "RPCFail_def",
thm "MClkReply_def", thm "Return_def", thm "Call_def", thm "e_def",
thm "c_def", thm "m_def", thm "caller_def", thm "rtrner_def", thm "S_def",
@@ -385,7 +385,7 @@
lemma S3Fail: "|- RPCFail crCh rmCh rst p & $(S3 rmhist p) & HNext rmhist p
& unchanged (e p, c p, m p)
--> (S6 rmhist p)$"
- by (tactic {* action_simp_tac (simpset () addsimps [thm "HNext_def",
+ by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
thm "RPCFail_def", thm "Return_def", thm "e_def", thm "c_def",
thm "m_def", thm "caller_def", thm "rtrner_def", thm "MVOKBARF_def",
thm "S_def", thm "S3_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
@@ -412,7 +412,7 @@
lemma S4ReadInner: "|- ReadInner rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
& HNext rmhist p & $(MemInv mm l)
--> (S4 rmhist p)$ & unchanged (rmhist!p)"
- by (tactic {* action_simp_tac (simpset () addsimps [thm "ReadInner_def",
+ by (tactic {* action_simp_tac (@{simpset} addsimps [thm "ReadInner_def",
thm "GoodRead_def", thm "BadRead_def", thm "HNext_def", thm "MemReturn_def",
thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "e_def",
thm "c_def", thm "r_def", thm "rtrner_def", thm "caller_def",
@@ -426,7 +426,7 @@
lemma S4WriteInner: "|- WriteInner rmCh mm ires p l v & $(S4 rmhist p) & unchanged (e p, c p, r p) & HNext rmhist p
--> (S4 rmhist p)$ & unchanged (rmhist!p)"
- by (tactic {* action_simp_tac (simpset () addsimps [thm "WriteInner_def",
+ by (tactic {* action_simp_tac (@{simpset} addsimps [thm "WriteInner_def",
thm "GoodWrite_def", thm "BadWrite_def", thm "HNext_def", thm "MemReturn_def",
thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "e_def",
thm "c_def", thm "r_def", thm "rtrner_def", thm "caller_def", thm "MVNROKBA_def",
@@ -465,14 +465,14 @@
lemma S5Reply: "|- RPCReply crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
--> (S6 rmhist p)$"
- by (tactic {* action_simp_tac (simpset () addsimps [thm "RPCReply_def",
+ by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCReply_def",
thm "Return_def", thm "e_def", thm "c_def", thm "m_def", thm "MVOKBA_def",
thm "MVOKBARF_def", thm "caller_def", thm "rtrner_def", thm "S_def",
thm "S5_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
lemma S5Fail: "|- RPCFail crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
--> (S6 rmhist p)$"
- by (tactic {* action_simp_tac (simpset () addsimps [thm "RPCFail_def",
+ by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFail_def",
thm "Return_def", thm "e_def", thm "c_def", thm "m_def",
thm "MVOKBARF_def", thm "caller_def", thm "rtrner_def",
thm "S_def", thm "S5_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
@@ -498,7 +498,7 @@
lemma S6Retry: "|- MClkRetry memCh crCh cst p & HNext rmhist p & $S6 rmhist p
& unchanged (e p,r p,m p)
--> (S3 rmhist p)$ & unchanged (rmhist!p)"
- by (tactic {* action_simp_tac (simpset () addsimps [thm "HNext_def",
+ by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
thm "MClkReply_def", thm "MClkRetry_def", thm "Call_def", thm "Return_def",
thm "e_def", thm "r_def", thm "m_def", thm "caller_def", thm "rtrner_def",
thm "S_def", thm "S6_def", thm "S3_def", thm "Calling_def"]) [] [] 1 *})
@@ -506,7 +506,7 @@
lemma S6Reply: "|- MClkReply memCh crCh cst p & HNext rmhist p & $S6 rmhist p
& unchanged (e p,r p,m p)
--> (S1 rmhist p)$"
- by (tactic {* action_simp_tac (simpset () addsimps [thm "HNext_def",
+ by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
thm "MemReturn_def", thm "RPCFail_def", thm "Return_def", thm "MClkReply_def",
thm "e_def", thm "r_def", thm "m_def", thm "caller_def", thm "rtrner_def",
thm "S_def", thm "S6_def", thm "S1_def", thm "Calling_def"]) [] [] 1 *})
@@ -538,7 +538,7 @@
lemma Step1_2_1: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
& ~unchanged (e p, c p, r p, m p, rmhist!p) & $S1 rmhist p
--> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
- apply (tactic {* action_simp_tac (simpset() addsimps [thm "ImpNext_def"]) []
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
(map temp_elim [thm "S1ClerkUnch", thm "S1RPCUnch", thm "S1MemUnch", thm "S1Hist"]) 1 *})
apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use (thm "S1Env")]) *})
done
@@ -547,7 +547,7 @@
& ~unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
--> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
& unchanged (e p, r p, m p, rmhist!p)"
- apply (tactic {* action_simp_tac (simpset() addsimps [thm "ImpNext_def"]) []
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
(map temp_elim [thm "S2EnvUnch", thm "S2RPCUnch", thm "S2MemUnch", thm "S2Hist"]) 1 *})
apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use (thm "S2Clerk"),
temp_use (thm "S2Forward")]) *})
@@ -557,9 +557,9 @@
& ~unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p
--> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p))
| ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
- apply (tactic {* action_simp_tac (simpset() addsimps [thm "ImpNext_def"]) []
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
(map temp_elim [thm "S3EnvUnch", thm "S3ClerkUnch", thm "S3MemUnch"]) 1 *})
- apply (tactic {* action_simp_tac (simpset()) []
+ apply (tactic {* action_simp_tac @{simpset} []
(thm "squareE" :: map temp_elim [thm "S3RPC", thm "S3Forward", thm "S3Fail"]) 1 *})
apply (auto dest!: S3Hist [temp_use])
done
@@ -570,9 +570,9 @@
--> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p))
| ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p))
| ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"
- apply (tactic {* action_simp_tac (simpset() addsimps [thm "ImpNext_def"]) []
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
(map temp_elim [thm "S4EnvUnch", thm "S4ClerkUnch", thm "S4RPCUnch"]) 1 *})
- apply (tactic {* action_simp_tac (simpset() addsimps [thm "RNext_def"]) []
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "RNext_def"]) []
(thm "squareE" :: map temp_elim [thm "S4Read", thm "S4Write", thm "S4Return"]) 1 *})
apply (auto dest!: S4Hist [temp_use])
done
@@ -581,9 +581,9 @@
& ~unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p
--> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p))
| ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
- apply (tactic {* action_simp_tac (simpset() addsimps [thm "ImpNext_def"]) []
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
(map temp_elim [thm "S5EnvUnch", thm "S5ClerkUnch", thm "S5MemUnch", thm "S5Hist"]) 1 *})
- apply (tactic {* action_simp_tac (simpset()) [] [thm "squareE", temp_elim (thm "S5RPC")] 1 *})
+ apply (tactic {* action_simp_tac @{simpset} [] [thm "squareE", temp_elim (thm "S5RPC")] 1 *})
apply (tactic {* auto_tac (MI_fast_css addSDs2
[temp_use (thm "S5Reply"), temp_use (thm "S5Fail")]) *})
done
@@ -592,9 +592,9 @@
& ~unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p
--> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))
| ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
- apply (tactic {* action_simp_tac (simpset() addsimps [thm "ImpNext_def"]) []
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
(map temp_elim [thm "S6EnvUnch", thm "S6RPCUnch", thm "S6MemUnch"]) 1 *})
- apply (tactic {* action_simp_tac (simpset()) []
+ apply (tactic {* action_simp_tac @{simpset} []
(thm "squareE" :: map temp_elim [thm "S6Clerk", thm "S6Retry", thm "S6Reply"]) 1 *})
apply (auto dest: S6Hist [temp_use])
done
@@ -606,7 +606,7 @@
section "Initialization (Step 1.3)"
lemma Step1_3: "|- S1 rmhist p --> PInit (resbar rmhist) p"
- by (tactic {* action_simp_tac (simpset () addsimps [thm "resbar_def",
+ by (tactic {* action_simp_tac (@{simpset} addsimps [thm "resbar_def",
thm "PInit_def", thm "S_def", thm "S1_def"]) [] [] 1 *})
(* ----------------------------------------------------------------------
@@ -625,7 +625,7 @@
& unchanged (e p, r p, m p, rmhist!p)
--> unchanged (rtrner memCh!p, resbar rmhist!p)"
by (tactic {* action_simp_tac
- (simpset() addsimps [thm "MClkFwd_def", thm "e_def", thm "r_def", thm "m_def",
+ (@{simpset} addsimps [thm "MClkFwd_def", thm "e_def", thm "r_def", thm "m_def",
thm "resbar_def", thm "S_def", thm "S2_def", thm "S3_def"]) [] [] 1 *})
lemma Step1_4_3a: "|- RPCFwd crCh rmCh rst p & $S3 rmhist p & (S4 rmhist p)$
@@ -633,7 +633,7 @@
--> unchanged (rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (drule S3_excl [temp_use] S4_excl [temp_use])+
- apply (tactic {* action_simp_tac (simpset () addsimps [thm "e_def",
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
thm "c_def", thm "m_def", thm "resbar_def", thm "S_def", thm "S3_def"]) [] [] 1 *})
done
@@ -652,11 +652,11 @@
--> ReadInner memCh mm (resbar rmhist) p l"
apply clarsimp
apply (drule S4_excl [temp_use])+
- apply (tactic {* action_simp_tac (simpset () addsimps [thm "ReadInner_def",
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ReadInner_def",
thm "GoodRead_def", thm "BadRead_def", thm "e_def", thm "c_def", thm "m_def"]) [] [] 1 *})
apply (auto simp: resbar_def)
apply (tactic {* ALLGOALS (action_simp_tac
- (simpset() addsimps [thm "RPCRelayArg_def", thm "MClkRelayArg_def",
+ (@{simpset} addsimps [thm "RPCRelayArg_def", thm "MClkRelayArg_def",
thm "S_def", thm "S4_def", thm "RdRequest_def", thm "MemInv_def"])
[] [thm "impE", thm "MemValNotAResultE"]) *})
done
@@ -671,11 +671,11 @@
--> WriteInner memCh mm (resbar rmhist) p l v"
apply clarsimp
apply (drule S4_excl [temp_use])+
- apply (tactic {* action_simp_tac (simpset () addsimps
+ apply (tactic {* action_simp_tac (@{simpset} addsimps
[thm "WriteInner_def", thm "GoodWrite_def", thm "BadWrite_def", thm "e_def",
thm "c_def", thm "m_def"]) [] [] 1 *})
apply (auto simp: resbar_def)
- apply (tactic {* ALLGOALS (action_simp_tac (simpset () addsimps
+ apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
[thm "RPCRelayArg_def", thm "MClkRelayArg_def", thm "S_def",
thm "S4_def", thm "WrRequest_def"]) [] []) *})
done
@@ -688,7 +688,7 @@
lemma Step1_4_4c: "|- MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$
& unchanged (e p, c p, r p)
--> unchanged (rtrner memCh!p, resbar rmhist!p)"
- apply (tactic {* action_simp_tac (simpset () addsimps [thm "e_def",
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
thm "c_def", thm "r_def", thm "resbar_def"]) [] [] 1 *})
apply (drule S4_excl [temp_use] S5_excl [temp_use])+
apply (tactic {* auto_tac (MI_fast_css addsimps2 [thm "MemReturn_def", thm "Return_def"]) *})
@@ -717,11 +717,11 @@
--> MemReturn memCh (resbar rmhist) p"
apply clarsimp
apply (drule S6_excl [temp_use])+
- apply (tactic {* action_simp_tac (simpset () addsimps [thm "e_def",
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
thm "r_def", thm "m_def", thm "MClkReply_def", thm "MemReturn_def",
thm "Return_def", thm "resbar_def"]) [] [] 1 *})
apply simp_all (* simplify if-then-else *)
- apply (tactic {* ALLGOALS (action_simp_tac (simpset () addsimps
+ apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
[thm "MClkReplyVal_def", thm "S6_def", thm "S_def"]) [] [thm "MVOKBARFnotNR"]) *})
done
@@ -730,7 +730,7 @@
--> MemFail memCh (resbar rmhist) p"
apply clarsimp
apply (drule S3_excl [temp_use])+
- apply (tactic {* action_simp_tac (simpset () addsimps [thm "e_def", thm "r_def",
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def", thm "r_def",
thm "m_def", thm "MClkRetry_def", thm "MemFail_def", thm "resbar_def"]) [] [] 1 *})
apply (auto simp: S6_def S_def)
done
@@ -862,14 +862,14 @@
lemma S1_RNextdisabled: "|- S1 rmhist p -->
~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
- apply (tactic {* action_simp_tac (simpset () addsimps [thm "angle_def",
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def",
thm "S_def", thm "S1_def"]) [notI] [thm "enabledE", temp_elim (thm "Memoryidle")] 1 *})
apply force
done
lemma S1_Returndisabled: "|- S1 rmhist p -->
~Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
- by (tactic {* action_simp_tac (simpset () addsimps [thm "angle_def", thm "MemReturn_def",
+ by (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def", thm "MemReturn_def",
thm "Return_def", thm "S_def", thm "S1_def"]) [notI] [thm "enabledE"] 1 *})
lemma RNext_fair: "|- []<>S1 rmhist p
@@ -1048,7 +1048,7 @@
lemma MClkReplyS6:
"|- $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) --> $S6 rmhist p"
- by (tactic {* action_simp_tac (simpset () addsimps [thm "angle_def",
+ by (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def",
thm "MClkReply_def", thm "Return_def", thm "ImpInv_def", thm "S_def",
thm "S1_def", thm "S2_def", thm "S3_def", thm "S4_def", thm "S5_def"]) [] [] 1 *})
@@ -1056,7 +1056,7 @@
apply (auto simp: c_def intro!: MClkReply_enabled [temp_use])
apply (cut_tac MI_base)
apply (blast dest: base_pair)
- apply (tactic {* ALLGOALS (action_simp_tac (simpset ()
+ apply (tactic {* ALLGOALS (action_simp_tac (@{simpset}
addsimps [thm "S_def", thm "S6_def"]) [] []) *})
done
@@ -1067,7 +1067,7 @@
apply (subgoal_tac "sigma |= []<> (<MClkReply memCh crCh cst p>_ (c p))")
apply (erule InfiniteEnsures)
apply assumption
- apply (tactic {* action_simp_tac (simpset()) []
+ apply (tactic {* action_simp_tac @{simpset} []
(map temp_elim [thm "MClkReplyS6", thm "S6MClkReply_successors"]) 1 *})
apply (auto simp: SF_def)
apply (erule contrapos_np)
@@ -1154,7 +1154,7 @@
sigma |= []<>S6 rmhist p --> []<>S1 rmhist p |]
==> sigma |= []<>S1 rmhist p"
apply (rule classical)
- apply (tactic {* asm_lr_simp_tac (simpset() addsimps
+ apply (tactic {* asm_lr_simp_tac (@{simpset} addsimps
[temp_use (thm "NotBox"), temp_rewrite (thm "NotDmd")]) 1 *})
apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use])
done
--- a/src/HOL/TLA/Memory/RPC.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/TLA/Memory/RPC.thy Wed Mar 19 22:50:42 2008 +0100
@@ -103,14 +103,14 @@
(* Enabledness of some actions *)
lemma RPCFail_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>
|- ~Calling rcv p & Calling send p --> Enabled (RPCFail send rcv rst p)"
- by (tactic {* action_simp_tac (simpset () addsimps [thm "RPCFail_def",
+ by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFail_def",
thm "Return_def", thm "caller_def", thm "rtrner_def"]) [exI]
[thm "base_enabled", thm "Pair_inject"] 1 *})
lemma RPCReply_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>
|- ~Calling rcv p & Calling send p & rst!p = #rpcB
--> Enabled (RPCReply send rcv rst p)"
- by (tactic {* action_simp_tac (simpset () addsimps [thm "RPCReply_def",
+ by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCReply_def",
thm "Return_def", thm "caller_def", thm "rtrner_def"]) [exI]
[thm "base_enabled", thm "Pair_inject"] 1 *})
--- a/src/HOL/W0/W0.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/W0/W0.thy Wed Mar 19 22:50:42 2008 +0100
@@ -196,15 +196,15 @@
apply (unfold new_tv_def)
apply (tactic "safe_tac HOL_cs")
-- {* @{text \<Longrightarrow>} *}
- apply (tactic {* fast_tac (HOL_cs addDs [@{thm leD}] addss (simpset()
+ apply (tactic {* fast_tac (HOL_cs addDs [@{thm leD}] addss (@{simpset}
addsimps [thm "free_tv_subst", thm "dom_def"])) 1 *})
apply (subgoal_tac "m \<in> cod s \<or> s l = TVar l")
apply (tactic "safe_tac HOL_cs")
- apply (tactic {* fast_tac (HOL_cs addDs [UnI2] addss (simpset()
+ apply (tactic {* fast_tac (HOL_cs addDs [UnI2] addss (@{simpset}
addsimps [thm "free_tv_subst"])) 1 *})
apply (drule_tac P = "\<lambda>x. m \<in> free_tv x" in subst, assumption)
apply simp
- apply (tactic {* fast_tac (set_cs addss (simpset()
+ apply (tactic {* fast_tac (set_cs addss (@{simpset}
addsimps [thm "free_tv_subst", thm "cod_def", thm "dom_def"])) 1 *})
-- {* @{text \<Longleftarrow>} *}
apply (unfold free_tv_subst cod_def dom_def)
@@ -350,7 +350,7 @@
apply (tactic {*
fast_tac (set_cs addSDs [thm "free_tv_app_subst_te" RS subsetD,
thm "free_tv_subst_var" RS subsetD]
- addss (simpset() delsimps (thms "bex_simps")
+ addss (@{simpset} delsimps (thms "bex_simps")
addsimps [thm "cod_def", thm "dom_def"])) 1 *})
done
@@ -555,7 +555,7 @@
new_tv_le)
apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
- addss (simpset())) 1 *})
+ addss @{simpset}) 1 *})
apply (rule lessI [THEN new_tv_subst_var])
apply (erule sym [THEN mgu_new])
apply (bestsimp intro!: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te
@@ -563,7 +563,7 @@
lessI [THEN less_imp_le, THEN new_tv_subst_le] new_tv_le)
apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
- addss (simpset())) 1 *})
+ addss @{simpset}) 1 *})
done
lemma free_tv_W: "!!n a s t m v. \<W> e a n = Ok (s, t, m) \<Longrightarrow>
@@ -616,7 +616,7 @@
thm "free_tv_subst_var" RS subsetD,
thm "free_tv_app_subst_te" RS subsetD,
thm "free_tv_app_subst_tel" RS subsetD, @{thm less_le_trans}, subsetD]
- addSEs [UnE] addss (simpset() setSolver unsafe_solver)) 1 *})
+ addSEs [UnE] addss (@{simpset} setSolver unsafe_solver)) 1 *})
-- {* builtin arithmetic in simpset messes things up *}
done
@@ -798,7 +798,7 @@
apply (simp add: app_subst_list split: split_if)
txt {* case @{text "Abs e"} *}
apply (tactic {* asm_full_simp_tac
- (simpset() setloop (split_inside_tac [thm "split_bind"])) 1 *})
+ (@{simpset} setloop (split_inside_tac [thm "split_bind"])) 1 *})
apply (intro strip)
apply (rule conjI)
apply (intro strip)
@@ -814,7 +814,7 @@
apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp,
thm "new_tv_subst_le", @{thm less_imp_le}, @{thm lessI}]) 1 *})
txt {* case @{text "App e1 e2"} *}
- apply (tactic {* simp_tac (simpset () setloop (split_inside_tac [thm "split_bind"])) 1 *})
+ apply (tactic {* simp_tac (@{simpset} setloop (split_inside_tac [thm "split_bind"])) 1 *})
apply (intro strip)
apply (rename_tac s1' t1 n1 s2' t2 n2 sa)
apply (rule conjI)
--- a/src/HOLCF/IOA/ABP/Correctness.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOLCF/IOA/ABP/Correctness.thy Wed Mar 19 22:50:42 2008 +0100
@@ -82,7 +82,7 @@
lemma last_ind_on_first:
"l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))"
apply simp
- apply (tactic {* auto_tac (claset(),
+ apply (tactic {* auto_tac (@{claset},
HOL_ss addsplits [thm"list.split"]
addsimps (thms "reverse.simps" @ [thm "hd_append", thm "rev_red_not_nil"])) *})
done
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Wed Mar 19 22:50:42 2008 +0100
@@ -6,7 +6,7 @@
Proof generator for domain command.
*)
-val HOLCF_ss = simpset();
+val HOLCF_ss = @{simpset};
structure Domain_Theorems = struct
@@ -113,7 +113,7 @@
val dist_eqI = prove_goal (the_context ()) "!!x::'a::po. ~ x << y ==> x ~= y"
(fn prems =>
- [blast_tac (claset () addDs [antisym_less_inverse]) 1]);
+ [blast_tac (@{claset} addDs [antisym_less_inverse]) 1]);
in
@@ -638,7 +638,7 @@
(* ----- theorems concerning finite approximation and finite induction ------ *)
local
- val iterate_Cprod_ss = simpset_of (theory "Fix");
+ val iterate_Cprod_ss = simpset_of @{theory Fix};
val copy_con_rews = copy_rews @ con_rews;
val copy_take_defs =
(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;