more antiquotations;
authorwenzelm
Wed Mar 19 22:50:42 2008 +0100 (2008-03-19)
changeset 263420f65fa163304
parent 26341 2f5a4367a39e
child 26343 0dd2eab7b296
more antiquotations;
src/CCL/CCL.thy
src/CCL/Term.thy
src/CCL/Type.thy
src/FOL/ex/Classical.thy
src/FOL/ex/Miniscope.thy
src/HOL/Algebra/abstract/Ideal2.thy
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Algebra/poly/LongDiv.thy
src/HOL/Auth/Message.thy
src/HOL/Bali/AxExample.thy
src/HOL/Bali/AxSem.thy
src/HOL/Bali/Example.thy
src/HOL/Fun.thy
src/HOL/HoareParallel/Gar_Coll.thy
src/HOL/HoareParallel/Mul_Gar_Coll.thy
src/HOL/IMP/VC.thy
src/HOL/IOA/Solve.thy
src/HOL/MicroJava/J/Conform.thy
src/HOL/Modelcheck/EindhovenSyn.thy
src/HOL/Modelcheck/MuckeSyn.thy
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/NatBin.thy
src/HOL/Nominal/Nominal.thy
src/HOL/SET-Protocol/MessageSET.thy
src/HOL/TLA/Buffer/DBuffer.thy
src/HOL/TLA/Inc/Inc.thy
src/HOL/TLA/Memory/MemClerk.thy
src/HOL/TLA/Memory/Memory.thy
src/HOL/TLA/Memory/MemoryImplementation.thy
src/HOL/TLA/Memory/RPC.thy
src/HOL/W0/W0.thy
src/HOLCF/IOA/ABP/Correctness.thy
src/HOLCF/Tools/domain/domain_theorems.ML
     1.1 --- a/src/CCL/CCL.thy	Wed Mar 19 22:47:39 2008 +0100
     1.2 +++ b/src/CCL/CCL.thy	Wed Mar 19 22:50:42 2008 +0100
     1.3 @@ -390,7 +390,7 @@
     1.4  local
     1.5    fun mk_thm s = prove_goal (the_context ()) s (fn _ =>
     1.6                            [rtac notI 1,dtac (thm "case_pocong") 1,etac rev_mp 5,
     1.7 -                           ALLGOALS (simp_tac (simpset ())),
     1.8 +                           ALLGOALS (simp_tac @{simpset}),
     1.9                             REPEAT (resolve_tac [thm "po_refl", thm "npo_lam_bot"] 1)])
    1.10  in
    1.11  
     2.1 --- a/src/CCL/Term.thy	Wed Mar 19 22:47:39 2008 +0100
     2.2 +++ b/src/CCL/Term.thy	Wed Mar 19 22:50:42 2008 +0100
     2.3 @@ -209,11 +209,11 @@
     2.4  
     2.5  fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s
     2.6             (fn _ => [stac letrecB 1,
     2.7 -                     simp_tac (simpset () addsimps rawBs) 1]);
     2.8 +                     simp_tac (@{simpset} addsimps rawBs) 1]);
     2.9  fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
    2.10  
    2.11  fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s
    2.12 -           (fn _ => [simp_tac (simpset () addsimps rawBs
    2.13 +           (fn _ => [simp_tac (@{simpset} addsimps rawBs
    2.14                                 setloop (stac letrecB)) 1]);
    2.15  fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
    2.16  
    2.17 @@ -298,7 +298,7 @@
    2.18  
    2.19  local
    2.20    fun mk_thm s = prove_goalw (the_context ()) (thms "data_defs") s (fn _ =>
    2.21 -    [simp_tac (simpset () addsimps (thms "ccl_porews")) 1])
    2.22 +    [simp_tac (@{simpset} addsimps (thms "ccl_porews")) 1])
    2.23  in
    2.24    val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
    2.25                                  "inr(b) [= inr(b') <-> b [= b'",
     3.1 --- a/src/CCL/Type.thy	Wed Mar 19 22:47:39 2008 +0100
     3.2 +++ b/src/CCL/Type.thy	Wed Mar 19 22:50:42 2008 +0100
     3.3 @@ -397,7 +397,7 @@
     3.4    val lfpI = thm "lfpI"
     3.5    val coinduct3_mono_lemma = thm "coinduct3_mono_lemma"
     3.6    fun mk_thm s = prove_goal (the_context ()) s (fn mono::prems =>
     3.7 -       [fast_tac (claset () addIs ((mono RS coinduct3_mono_lemma RS lfpI)::prems)) 1])
     3.8 +       [fast_tac (@{claset} addIs ((mono RS coinduct3_mono_lemma RS lfpI)::prems)) 1])
     3.9  in
    3.10  val ci3_RI    = mk_thm "[|  mono(Agen);  a : R |] ==> a : lfp(%x. Agen(x) Un R Un A)"
    3.11  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)"
    3.12 @@ -405,8 +405,8 @@
    3.13  
    3.14  fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s
    3.15        (fn prems => [rtac (genXH RS iffD2) 1,
    3.16 -                    simp_tac (simpset ()) 1,
    3.17 -                    TRY (fast_tac (claset () addIs
    3.18 +                    SIMPSET' simp_tac 1,
    3.19 +                    TRY (fast_tac (@{claset} addIs
    3.20                              ([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI]
    3.21                               @ prems)) 1)])
    3.22  end;
     4.1 --- a/src/FOL/ex/Classical.thy	Wed Mar 19 22:47:39 2008 +0100
     4.2 +++ b/src/FOL/ex/Classical.thy	Wed Mar 19 22:50:42 2008 +0100
     4.3 @@ -459,7 +459,7 @@
     4.4                    ((C(y) & Q(w,y,y)) & OO(w,b) --> P(v,y) & OO(v,b)))))  
     4.5     -->                   
     4.6     ~ (\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z))))"
     4.7 -by (tactic{*Blast.depth_tac (claset ()) 12 1*})
     4.8 +by (tactic{*Blast.depth_tac @{claset} 12 1*})
     4.9     --{*Needed because the search for depths below 12 is very slow*}
    4.10  
    4.11  
     5.1 --- a/src/FOL/ex/Miniscope.thy	Wed Mar 19 22:47:39 2008 +0100
     5.2 +++ b/src/FOL/ex/Miniscope.thy	Wed Mar 19 22:50:42 2008 +0100
     5.3 @@ -65,8 +65,8 @@
     5.4  lemmas mini_simps = demorgans nnf_simps ex_simps all_simps
     5.5  
     5.6  ML {*
     5.7 -val mini_ss = simpset() addsimps (thms "mini_simps");
     5.8 -val mini_tac = rtac (thm "ccontr") THEN' asm_full_simp_tac mini_ss;
     5.9 +val mini_ss = @{simpset} addsimps @{thms mini_simps};
    5.10 +val mini_tac = rtac @{thm ccontr} THEN' asm_full_simp_tac mini_ss;
    5.11  *}
    5.12  
    5.13  end
     6.1 --- a/src/HOL/Algebra/abstract/Ideal2.thy	Wed Mar 19 22:47:39 2008 +0100
     6.2 +++ b/src/HOL/Algebra/abstract/Ideal2.thy	Wed Mar 19 22:50:42 2008 +0100
     6.3 @@ -115,8 +115,8 @@
     6.4     apply (rule subsetI)
     6.5     apply (drule InterD)
     6.6      prefer 2 apply assumption
     6.7 -   apply (tactic {* auto_tac (claset() addIs [thm "is_ideal_2"],
     6.8 -     simpset() delsimprocs [ring_simproc]) *})
     6.9 +   apply (tactic {* auto_tac (@{claset} addIs [@{thm is_ideal_2}],
    6.10 +     @{simpset} delsimprocs [ring_simproc]) *})
    6.11     apply (rule_tac x = "1" in exI)
    6.12     apply (rule_tac x = "0" in exI)
    6.13     apply (rule_tac [2] x = "0" in exI)
    6.14 @@ -283,7 +283,7 @@
    6.15    apply (drule_tac f = "op* aa" in arg_cong)
    6.16    apply (simp add: r_distr)
    6.17    apply (erule subst)
    6.18 -  apply (tactic {* asm_simp_tac (simpset() addsimps [thm "m_assoc" RS sym]
    6.19 +  apply (tactic {* asm_simp_tac (@{simpset} addsimps [@{thm m_assoc} RS sym]
    6.20      delsimprocs [ring_simproc]) 1 *})
    6.21    done
    6.22  
     7.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Wed Mar 19 22:47:39 2008 +0100
     7.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Wed Mar 19 22:50:42 2008 +0100
     7.3 @@ -465,7 +465,7 @@
     7.4  
     7.5  lemma r_inverse_ring: "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1"
     7.6    apply (unfold inverse_def dvd_def)
     7.7 -  apply (tactic {* asm_full_simp_tac (simpset () delsimprocs [ring_simproc]) 1 *})
     7.8 +  apply (tactic {* asm_full_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *})
     7.9    apply clarify
    7.10    apply (rule theI)
    7.11     apply assumption
     8.1 --- a/src/HOL/Algebra/poly/LongDiv.thy	Wed Mar 19 22:47:39 2008 +0100
     8.2 +++ b/src/HOL/Algebra/poly/LongDiv.thy	Wed Mar 19 22:50:42 2008 +0100
     8.3 @@ -129,16 +129,16 @@
     8.4    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)
     8.5    apply clarify
     8.6    apply (drule sym)
     8.7 -  apply (tactic {* simp_tac (simpset() addsimps [thm "l_distr", thm "a_assoc"]
     8.8 +  apply (tactic {* simp_tac (@{simpset} addsimps [@{thm l_distr}, @{thm a_assoc}]
     8.9      delsimprocs [ring_simproc]) 1 *})
    8.10 -  apply (tactic {* asm_simp_tac (simpset() delsimprocs [ring_simproc]) 1 *})
    8.11 -  apply (tactic {* simp_tac (simpset () addsimps [thm "minus_def", thm "smult_r_distr",
    8.12 +  apply (tactic {* asm_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *})
    8.13 +  apply (tactic {* simp_tac (@{simpset} addsimps [thm "minus_def", thm "smult_r_distr",
    8.14      thm "smult_r_minus", thm "monom_mult_smult", thm "smult_assoc1", thm "smult_assoc2"]
    8.15      delsimprocs [ring_simproc]) 1 *})
    8.16    apply simp
    8.17    done
    8.18  
    8.19 -ML {* simplify (simpset() addsimps [thm "eucl_size_def"]
    8.20 +ML {* simplify (@{simpset} addsimps [thm "eucl_size_def"]
    8.21      delsimprocs [ring_simproc]) (thm "long_div_eucl_size") *}
    8.22  
    8.23  thm long_div_eucl_size [simplified]
    8.24 @@ -148,9 +148,9 @@
    8.25       Ex (% (q, r, k).  
    8.26         (lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))"
    8.27    apply (tactic {* forw_inst_tac [("f", "f")]
    8.28 -    (simplify (simpset() addsimps [thm "eucl_size_def"]
    8.29 +    (simplify (@{simpset} addsimps [thm "eucl_size_def"]
    8.30        delsimprocs [ring_simproc]) (thm "long_div_eucl_size")) 1 *})
    8.31 -  apply (tactic {* auto_tac (claset(), simpset() delsimprocs [ring_simproc]) *})
    8.32 +  apply (tactic {* auto_tac (@{claset}, @{simpset} delsimprocs [ring_simproc]) *})
    8.33    apply (case_tac "aa = 0")
    8.34     apply blast
    8.35    (* case "aa ~= 0 *)
    8.36 @@ -169,7 +169,7 @@
    8.37    apply (rule conjI)
    8.38     apply (drule sym)
    8.39     apply (tactic {* asm_simp_tac
    8.40 -     (simpset() addsimps [thm "smult_r_distr" RS sym, thm "smult_assoc2"]
    8.41 +     (@{simpset} addsimps [thm "smult_r_distr" RS sym, thm "smult_assoc2"]
    8.42       delsimprocs [ring_simproc]) 1 *})
    8.43     apply (simp (no_asm_simp) add: l_inverse_ring unit_power smult_assoc1 [symmetric])
    8.44    (* degree property *)
    8.45 @@ -194,7 +194,7 @@
    8.46  
    8.47  lemma diff_zero_imp_eq: "!!a::'a::ring. a - b = 0 ==> a = b"
    8.48    apply (rule_tac s = "a - (a - b) " in trans)
    8.49 -   apply (tactic {* asm_simp_tac (simpset() delsimprocs [ring_simproc]) 1 *})
    8.50 +   apply (tactic {* asm_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *})
    8.51     apply simp
    8.52    apply (simp (no_asm))
    8.53    done
    8.54 @@ -215,22 +215,22 @@
    8.55    (* r1 = 0 *)
    8.56      apply (erule disjE)
    8.57    (* r2 = 0 *)
    8.58 -     apply (tactic {* asm_full_simp_tac (simpset()
    8.59 +     apply (tactic {* asm_full_simp_tac (@{simpset}
    8.60         addsimps [thm "integral_iff", thm "minus_def", thm "l_zero", thm "uminus_zero"]
    8.61         delsimprocs [ring_simproc]) 1 *})
    8.62    (* r2 ~= 0 *)
    8.63      apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
    8.64 -    apply (tactic {* asm_full_simp_tac (simpset() addsimps
    8.65 +    apply (tactic {* asm_full_simp_tac (@{simpset} addsimps
    8.66        [thm "minus_def", thm "l_zero", thm "uminus_zero"] delsimprocs [ring_simproc]) 1 *})
    8.67    (* r1 ~=0 *)
    8.68     apply (erule disjE)
    8.69    (* r2 = 0 *)
    8.70      apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
    8.71 -    apply (tactic {* asm_full_simp_tac (simpset() addsimps
    8.72 +    apply (tactic {* asm_full_simp_tac (@{simpset} addsimps
    8.73        [thm "minus_def", thm "l_zero", thm "uminus_zero"] delsimprocs [ring_simproc]) 1 *})
    8.74    (* r2 ~= 0 *)
    8.75     apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
    8.76 -   apply (tactic {* asm_full_simp_tac (simpset() addsimps [thm "minus_def"]
    8.77 +   apply (tactic {* asm_full_simp_tac (@{simpset} addsimps [thm "minus_def"]
    8.78       delsimprocs [ring_simproc]) 1 *})
    8.79     apply (drule order_eq_refl [THEN add_leD2])
    8.80     apply (drule leD)
     9.1 --- a/src/HOL/Auth/Message.thy	Wed Mar 19 22:47:39 2008 +0100
     9.2 +++ b/src/HOL/Auth/Message.thy	Wed Mar 19 22:50:42 2008 +0100
     9.3 @@ -847,8 +847,8 @@
     9.4    concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
     9.5    alone.*)
     9.6  fun prove_simple_subgoals_tac i = 
     9.7 -    force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN
     9.8 -    ALLGOALS Asm_simp_tac
     9.9 +    CLASIMPSET' (fn (cs, ss) => force_tac (cs, ss addsimps [@{thm image_eq_UN}])) i THEN
    9.10 +    ALLGOALS (SIMPSET' asm_simp_tac)
    9.11  
    9.12  (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
    9.13    but this application is no longer necessary if analz_insert_eq is used.
    9.14 @@ -886,7 +886,7 @@
    9.15         REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
    9.16         DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
    9.17  
    9.18 -fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
    9.19 +val spy_analz_tac = CLASIMPSET' gen_spy_analz_tac;
    9.20  
    9.21  end
    9.22  *}
    10.1 --- a/src/HOL/Bali/AxExample.thy	Wed Mar 19 22:47:39 2008 +0100
    10.2 +++ b/src/HOL/Bali/AxExample.thy	Wed Mar 19 22:50:42 2008 +0100
    10.3 @@ -136,7 +136,7 @@
    10.4  apply       (rule ax_subst_Var_allI)
    10.5  apply       (tactic {* inst1_tac "P'" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
    10.6  apply       (rule allI)
    10.7 -apply       (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *})
    10.8 +apply       (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *})
    10.9  apply       (rule ax_derivs.Abrupt)
   10.10  apply      (simp (no_asm))
   10.11  apply      (tactic "ax_tac 1" (* FVar *))
   10.12 @@ -186,26 +186,26 @@
   10.13  apply  (rule ax_InitS)
   10.14  apply     force
   10.15  apply    (simp (no_asm))
   10.16 -apply   (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
   10.17 +apply   (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *})
   10.18  apply   (rule ax_Init_Skip_lemma)
   10.19 -apply  (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
   10.20 +apply  (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *})
   10.21  apply  (rule ax_InitS [THEN conseq1] (* init Base *))
   10.22  apply      force
   10.23  apply     (simp (no_asm))
   10.24  apply    (unfold arr_viewed_from_def)
   10.25  apply    (rule allI)
   10.26  apply    (rule_tac P' = "Normal ?P" in conseq1)
   10.27 -apply     (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
   10.28 +apply     (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *})
   10.29  apply     (tactic "ax_tac 1")
   10.30  apply     (tactic "ax_tac 1")
   10.31  apply     (rule_tac [2] ax_subst_Var_allI)
   10.32  apply      (tactic {* inst1_tac "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
   10.33 -apply     (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [split_paired_All, thm "peek_and_def2"]) 2 *})
   10.34 +apply     (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [split_paired_All, thm "peek_and_def2"]) 2 *})
   10.35  apply      (tactic "ax_tac 2" (* NewA *))
   10.36  apply       (tactic "ax_tac 3" (* ax_Alloc_Arr *))
   10.37  apply       (tactic "ax_tac 3")
   10.38  apply      (tactic {* inst1_tac "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *})
   10.39 -apply      (tactic {* simp_tac (simpset() delloop "split_all_tac") 2 *})
   10.40 +apply      (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 2 *})
   10.41  apply      (tactic "ax_tac 2")
   10.42  apply     (tactic "ax_tac 1" (* FVar *))
   10.43  apply      (tactic "ax_tac 2" (* StatRef *))
   10.44 @@ -216,7 +216,7 @@
   10.45  apply     (drule initedD)
   10.46  apply     (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def)
   10.47  apply    force
   10.48 -apply   (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
   10.49 +apply   (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *})
   10.50  apply   (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
   10.51  apply     (rule wf_tprg)
   10.52  apply    clarsimp
    11.1 --- a/src/HOL/Bali/AxSem.thy	Wed Mar 19 22:47:39 2008 +0100
    11.2 +++ b/src/HOL/Bali/AxSem.thy	Wed Mar 19 22:50:42 2008 +0100
    11.3 @@ -699,7 +699,7 @@
    11.4  (*42 subgoals*)
    11.5  apply       (tactic "ALLGOALS strip_tac")
    11.6  apply       (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"),
    11.7 -         etac disjE, fast_tac (claset() addSIs [thm "ax_derivs.empty"])]))*})
    11.8 +         etac disjE, fast_tac (@{claset} addSIs [thm "ax_derivs.empty"])]))*})
    11.9  apply       (tactic "TRYALL hyp_subst_tac")
   11.10  apply       (simp, rule ax_derivs.empty)
   11.11  apply      (drule subset_insertD)
    12.1 --- a/src/HOL/Bali/Example.thy	Wed Mar 19 22:47:39 2008 +0100
    12.2 +++ b/src/HOL/Bali/Example.thy	Wed Mar 19 22:50:42 2008 +0100
    12.3 @@ -1193,7 +1193,7 @@
    12.4          Base_foo_defs  [simp]
    12.5  
    12.6  ML_setup {* bind_thms ("eval_intros", map 
    12.7 -        (simplify (simpset() delsimps @{thms Skip_eq}
    12.8 +        (simplify (@{simpset} delsimps @{thms Skip_eq}
    12.9                               addsimps @{thms lvar_def}) o 
   12.10           rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
   12.11  lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
    13.1 --- a/src/HOL/Fun.thy	Wed Mar 19 22:47:39 2008 +0100
    13.2 +++ b/src/HOL/Fun.thy	Wed Mar 19 22:50:42 2008 +0100
    13.3 @@ -532,7 +532,7 @@
    13.4  subsection {* ML legacy bindings *} 
    13.5  
    13.6  ML {*
    13.7 -val set_cs = claset() delrules [equalityI]
    13.8 +val set_cs = @{claset} delrules [@{thm equalityI}]
    13.9  *}
   13.10  
   13.11  ML {*
    14.1 --- a/src/HOL/HoareParallel/Gar_Coll.thy	Wed Mar 19 22:47:39 2008 +0100
    14.2 +++ b/src/HOL/HoareParallel/Gar_Coll.thy	Wed Mar 19 22:50:42 2008 +0100
    14.3 @@ -796,9 +796,9 @@
    14.4  apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
    14.5  apply(tactic {* TRYALL (etac disjE) *})
    14.6  apply simp_all
    14.7 -apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac (thm "Graph3"),force_tac (clasimpset ()), assume_tac]) *})
    14.8 -apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
    14.9 -apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
   14.10 +apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{clasimpset}, assume_tac]) *})
   14.11 +apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{clasimpset}]) *})
   14.12 +apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{clasimpset}]) *})
   14.13  done
   14.14  
   14.15  subsubsection {* Interference freedom Mutator-Collector *}
    15.1 --- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Wed Mar 19 22:47:39 2008 +0100
    15.2 +++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Wed Mar 19 22:50:42 2008 +0100
    15.3 @@ -1200,7 +1200,7 @@
    15.4  --{* 72 subgoals left *}
    15.5  apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
    15.6  --{* 35 subgoals left *}
    15.7 -apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac (thm "Graph3"),force_tac (clasimpset ()), assume_tac]) *})
    15.8 +apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{clasimpset}, assume_tac]) *})
    15.9  --{* 28 subgoals left *}
   15.10  apply(tactic {* TRYALL (etac conjE) *})
   15.11  apply(tactic {* TRYALL (etac disjE) *})
   15.12 @@ -1210,17 +1210,17 @@
   15.13  apply(tactic {* ALLGOALS(case_tac "M x!(T (Muts x ! j))=Black") *})
   15.14  apply(simp_all add:Graph10)
   15.15  --{* 47 subgoals left *}
   15.16 -apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *})
   15.17 +apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
   15.18  --{* 41 subgoals left *}
   15.19 -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"])]) *})
   15.20 +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}])]) *})
   15.21  --{* 35 subgoals left *}
   15.22 -apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
   15.23 +apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac @{clasimpset}]) *})
   15.24  --{* 31 subgoals left *}
   15.25 -apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *})
   15.26 +apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
   15.27  --{* 29 subgoals left *}
   15.28 -apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *})
   15.29 +apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
   15.30  --{* 25 subgoals left *}
   15.31 -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"])]) *})
   15.32 +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}])]) *})
   15.33  --{* 10 subgoals left *}
   15.34  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)+
   15.35  done
    16.1 --- a/src/HOL/IMP/VC.thy	Wed Mar 19 22:47:39 2008 +0100
    16.2 +++ b/src/HOL/IMP/VC.thy	Wed Mar 19 22:50:42 2008 +0100
    16.3 @@ -77,7 +77,7 @@
    16.4    apply fast
    16.5   (* if *)
    16.6   apply atomize
    16.7 - apply (tactic "Deepen_tac 4 1")
    16.8 + apply (tactic "deepen_tac @{claset} 4 1")
    16.9  (* while *)
   16.10  apply atomize
   16.11  apply (intro allI impI)
    17.1 --- a/src/HOL/IOA/Solve.thy	Wed Mar 19 22:47:39 2008 +0100
    17.2 +++ b/src/HOL/IOA/Solve.thy	Wed Mar 19 22:50:42 2008 +0100
    17.3 @@ -149,7 +149,7 @@
    17.4    apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: split_if)
    17.5    apply (tactic {*
    17.6      REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
    17.7 -      asm_full_simp_tac(simpset() addsimps[thm "comp1_reachable", thm "comp2_reachable"]) 1) *})
    17.8 +      asm_full_simp_tac(@{simpset} addsimps[thm "comp1_reachable", thm "comp2_reachable"]) 1) *})
    17.9    done
   17.10  
   17.11  
    18.1 --- a/src/HOL/MicroJava/J/Conform.thy	Wed Mar 19 22:47:39 2008 +0100
    18.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Wed Mar 19 22:50:42 2008 +0100
    18.3 @@ -343,7 +343,7 @@
    18.4  apply(rule hconfI)
    18.5  apply(drule conforms_heapD)
    18.6  apply(tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"] 
    18.7 -                addDs [thm "hconfD"], simpset() delsimps [split_paired_All]) *})
    18.8 +                addDs [thm "hconfD"], @{simpset} delsimps [split_paired_All]) *})
    18.9  done
   18.10  
   18.11  lemma conforms_upd_local: 
    19.1 --- a/src/HOL/Modelcheck/EindhovenSyn.thy	Wed Mar 19 22:47:39 2008 +0100
    19.2 +++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Wed Mar 19 22:50:42 2008 +0100
    19.3 @@ -72,7 +72,7 @@
    19.4    (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
    19.5  
    19.6  val Eindhoven_ss =
    19.7 -  simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
    19.8 +  @{simpset} addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
    19.9  
   19.10  (*check if user has pmu installed*)
   19.11  fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> "";
    20.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy	Wed Mar 19 22:47:39 2008 +0100
    20.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy	Wed Mar 19 22:50:42 2008 +0100
    20.3 @@ -221,7 +221,7 @@
    20.4    Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
    20.5    (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
    20.6  
    20.7 -val Mucke_ss = simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
    20.8 +val Mucke_ss = @{simpset} addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
    20.9  
   20.10  
   20.11  (* the interface *)
    21.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Wed Mar 19 22:47:39 2008 +0100
    21.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Wed Mar 19 22:50:42 2008 +0100
    21.3 @@ -111,7 +111,7 @@
    21.4  (
    21.5  OldGoals.push_proof();
    21.6  OldGoals.goalw_cterm [] (cterm_of sign trm);
    21.7 -by (simp_tac (simpset()) 1);
    21.8 +by (SIMPSET' simp_tac 1);
    21.9          let
   21.10          val if_tmp_result = result()
   21.11          in
    22.1 --- a/src/HOL/NatBin.thy	Wed Mar 19 22:47:39 2008 +0100
    22.2 +++ b/src/HOL/NatBin.thy	Wed Mar 19 22:50:42 2008 +0100
    22.3 @@ -625,7 +625,7 @@
    22.4  
    22.5  ML
    22.6  {*
    22.7 -val numeral_ss = simpset() addsimps @{thms numerals};
    22.8 +val numeral_ss = @{simpset} addsimps @{thms numerals};
    22.9  
   22.10  val nat_bin_arith_setup =
   22.11   LinArith.map_data
    23.1 --- a/src/HOL/Nominal/Nominal.thy	Wed Mar 19 22:47:39 2008 +0100
    23.2 +++ b/src/HOL/Nominal/Nominal.thy	Wed Mar 19 22:50:42 2008 +0100
    23.3 @@ -386,9 +386,11 @@
    23.4    and   "a\<sharp>(x,y) \<Longrightarrow> a\<sharp>y"
    23.5    by (simp_all add: fresh_prod)
    23.6  
    23.7 -ML_setup {*
    23.8 -  val mksimps_pairs = ("Nominal.fresh", thms "fresh_prodD")::mksimps_pairs;
    23.9 -  change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs));
   23.10 +ML {*
   23.11 +  val mksimps_pairs = (@{const_name Nominal.fresh}, @{thms fresh_prodD}) :: mksimps_pairs;
   23.12 +*}
   23.13 +declaration {* fn _ =>
   23.14 +  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
   23.15  *}
   23.16  
   23.17  
    24.1 --- a/src/HOL/SET-Protocol/MessageSET.thy	Wed Mar 19 22:47:39 2008 +0100
    24.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy	Wed Mar 19 22:50:42 2008 +0100
    24.3 @@ -844,8 +844,8 @@
    24.4    concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
    24.5    alone.*)
    24.6  fun prove_simple_subgoals_tac i =
    24.7 -    force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN
    24.8 -    ALLGOALS Asm_simp_tac
    24.9 +    CLASIMPSET' (fn (cs, ss) => force_tac (cs, ss addsimps [@{thm image_eq_UN}])) i THEN
   24.10 +    ALLGOALS (SIMPSET' asm_simp_tac)
   24.11  
   24.12  (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
   24.13    but this application is no longer necessary if analz_insert_eq is used.
   24.14 @@ -883,7 +883,7 @@
   24.15         REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
   24.16         DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
   24.17  
   24.18 -fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
   24.19 +val spy_analz_tac = CLASIMPSET' gen_spy_analz_tac;
   24.20  
   24.21  end
   24.22  *}
    25.1 --- a/src/HOL/TLA/Buffer/DBuffer.thy	Wed Mar 19 22:47:39 2008 +0100
    25.2 +++ b/src/HOL/TLA/Buffer/DBuffer.thy	Wed Mar 19 22:50:42 2008 +0100
    25.3 @@ -63,7 +63,7 @@
    25.4    apply (rule square_simulation)
    25.5     apply clarsimp
    25.6    apply (tactic
    25.7 -    {* action_simp_tac (simpset () addsimps (thm "hd_append" :: thms "db_defs")) [] [] 1 *})
    25.8 +    {* action_simp_tac (@{simpset} addsimps (@{thm hd_append} :: @{thms db_defs})) [] [] 1 *})
    25.9    done
   25.10  
   25.11  
    26.1 --- a/src/HOL/TLA/Inc/Inc.thy	Wed Mar 19 22:47:39 2008 +0100
    26.2 +++ b/src/HOL/TLA/Inc/Inc.thy	Wed Mar 19 22:50:42 2008 +0100
    26.3 @@ -115,7 +115,7 @@
    26.4    by (auto simp: PsiInv_defs)
    26.5  
    26.6  lemma PsiInv: "|- Psi --> []PsiInv"
    26.7 -  apply (tactic {* inv_tac (clasimpset () addsimps2 [thm "Psi_def"]) 1 *})
    26.8 +  apply (tactic {* inv_tac (@{clasimpset} addsimps2 [@{thm Psi_def}]) 1 *})
    26.9     apply (force simp: PsiInv_Init [try_rewrite] Init_def)
   26.10    apply (auto intro: PsiInv_alpha1 [try_rewrite] PsiInv_alpha2 [try_rewrite]
   26.11      PsiInv_beta1 [try_rewrite] PsiInv_beta2 [try_rewrite] PsiInv_gamma1 [try_rewrite]
   26.12 @@ -128,7 +128,7 @@
   26.13  *)
   26.14  
   26.15  lemma "|- Psi --> []PsiInv"
   26.16 -  by (tactic {* auto_inv_tac (simpset() addsimps (thms "PsiInv_defs" @ thms "Psi_defs")) 1 *})
   26.17 +  by (tactic {* auto_inv_tac (@{simpset} addsimps (@{thms PsiInv_defs} @ @{thms Psi_defs})) 1 *})
   26.18  
   26.19  
   26.20  (**** Step simulation ****)
   26.21 @@ -174,9 +174,9 @@
   26.22      --> (pc1 = #g ~> pc1 = #a)"
   26.23    apply (rule SF1)
   26.24      apply (tactic
   26.25 -      {* action_simp_tac (simpset () addsimps (thms "Psi_defs")) [] [thm "squareE"] 1 *})
   26.26 +      {* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
   26.27     apply (tactic
   26.28 -      {* action_simp_tac (simpset () addsimps (thm "angle_def" :: thms "Psi_defs")) [] [] 1 *})
   26.29 +      {* action_simp_tac (@{simpset} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
   26.30    (* reduce |- []A --> <>Enabled B  to  |- A --> Enabled B *)
   26.31    apply (auto intro!: InitDmd_gen [temp_use] N1_enabled_at_g [temp_use]
   26.32      dest!: STL2_gen [temp_use] simp: Init_def)
   26.33 @@ -195,8 +195,8 @@
   26.34    "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True  
   26.35      --> (pc2 = #g ~> pc2 = #a)"
   26.36    apply (rule SF1)
   26.37 -  apply (tactic {* action_simp_tac (simpset () addsimps (thms "Psi_defs")) [] [thm "squareE"] 1 *})
   26.38 -  apply (tactic {* action_simp_tac (simpset () addsimps (thm "angle_def" :: thms "Psi_defs"))
   26.39 +  apply (tactic {* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
   26.40 +  apply (tactic {* action_simp_tac (@{simpset} addsimps @{thm angle_def} :: @{thms Psi_defs})
   26.41      [] [] 1 *})
   26.42    apply (auto intro!: InitDmd_gen [temp_use] N2_enabled_at_g [temp_use]
   26.43      dest!: STL2_gen [temp_use] simp add: Init_def)
   26.44 @@ -215,9 +215,9 @@
   26.45      --> (pc2 = #b ~> pc2 = #g)"
   26.46    apply (rule SF1)
   26.47      apply (tactic
   26.48 -      {* action_simp_tac (simpset () addsimps (thms "Psi_defs")) [] [thm "squareE"] 1 *})
   26.49 +      {* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
   26.50     apply (tactic
   26.51 -     {* action_simp_tac (simpset () addsimps (thm "angle_def" :: thms "Psi_defs")) [] [] 1 *})
   26.52 +     {* action_simp_tac (@{simpset} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
   26.53    apply (auto intro!: InitDmd_gen [temp_use] N2_enabled_at_b [temp_use]
   26.54      dest!: STL2_gen [temp_use] simp: Init_def)
   26.55    done
   26.56 @@ -257,9 +257,9 @@
   26.57           & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)   
   26.58           --> (pc1 = #a ~> pc1 = #b)"
   26.59    apply (rule SF1)
   26.60 -  apply (tactic {* action_simp_tac (simpset () addsimps thms "Psi_defs") [] [thm "squareE"] 1 *})
   26.61 +  apply (tactic {* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
   26.62    apply (tactic
   26.63 -    {* action_simp_tac (simpset () addsimps (thm "angle_def" :: thms "Psi_defs")) [] [] 1 *})
   26.64 +    {* action_simp_tac (@{simpset} addsimps (@{thm angle_def} :: @{thms Psi_defs})) [] [] 1 *})
   26.65    apply (clarsimp intro!: N1_enabled_at_both_a [THEN DmdImpl [temp_use]])
   26.66    apply (auto intro!: BoxDmd2_simple [temp_use] N2_live [temp_use]
   26.67      simp: split_box_conj more_temp_simps)
    27.1 --- a/src/HOL/TLA/Memory/MemClerk.thy	Wed Mar 19 22:47:39 2008 +0100
    27.2 +++ b/src/HOL/TLA/Memory/MemClerk.thy	Wed Mar 19 22:50:42 2008 +0100
    27.3 @@ -84,7 +84,7 @@
    27.4  lemma MClkFwd_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>  
    27.5        |- Calling send p & ~Calling rcv p & cst!p = #clkA   
    27.6           --> Enabled (MClkFwd send rcv cst p)"
    27.7 -  by (tactic {* action_simp_tac (simpset () addsimps [thm "MClkFwd_def",
    27.8 +  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "MClkFwd_def",
    27.9      thm "Call_def", thm "caller_def", thm "rtrner_def"]) [exI]
   27.10      [thm "base_enabled", Pair_inject] 1 *})
   27.11  
   27.12 @@ -99,9 +99,9 @@
   27.13  lemma MClkReply_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>  
   27.14        |- Calling send p & ~Calling rcv p & cst!p = #clkB   
   27.15           --> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
   27.16 -  apply (tactic {* action_simp_tac (simpset ())
   27.17 +  apply (tactic {* action_simp_tac @{simpset}
   27.18      [thm "MClkReply_change" RSN (2, thm "enabled_mono") ] [] 1 *})
   27.19 -  apply (tactic {* action_simp_tac (simpset () addsimps
   27.20 +  apply (tactic {* action_simp_tac (@{simpset} addsimps
   27.21      [thm "MClkReply_def", thm "Return_def", thm "caller_def", thm "rtrner_def"])
   27.22      [exI] [thm "base_enabled", Pair_inject] 1 *})
   27.23    done
    28.1 --- a/src/HOL/TLA/Memory/Memory.thy	Wed Mar 19 22:47:39 2008 +0100
    28.2 +++ b/src/HOL/TLA/Memory/Memory.thy	Wed Mar 19 22:50:42 2008 +0100
    28.3 @@ -152,7 +152,7 @@
    28.4  (* The memory spec implies the memory invariant *)
    28.5  lemma MemoryInvariant: "|- MSpec ch mm rs l --> [](MemInv mm l)"
    28.6    by (tactic {* auto_inv_tac
    28.7 -    (simpset () addsimps (thms "RM_temp_defs" @ thms "RM_action_defs")) 1 *})
    28.8 +    (@{simpset} addsimps (@{thms RM_temp_defs} @ @{thms RM_action_defs})) 1 *})
    28.9  
   28.10  (* The invariant is trivial for non-locations *)
   28.11  lemma NonMemLocInvariant: "|- #l ~: #MemLoc --> [](MemInv mm l)"
   28.12 @@ -182,9 +182,9 @@
   28.13        |- Calling ch p & (rs!p ~= #NotAResult)
   28.14           --> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))"
   28.15    apply (tactic
   28.16 -    {* action_simp_tac (simpset ()) [thm "MemReturn_change" RSN (2, thm "enabled_mono") ] [] 1 *})
   28.17 +    {* action_simp_tac @{simpset} [thm "MemReturn_change" RSN (2, thm "enabled_mono") ] [] 1 *})
   28.18    apply (tactic
   28.19 -    {* action_simp_tac (simpset () addsimps [thm "MemReturn_def", thm "Return_def",
   28.20 +    {* action_simp_tac (@{simpset} addsimps [thm "MemReturn_def", thm "Return_def",
   28.21        thm "rtrner_def"]) [exI] [thm "base_enabled", thm "Pair_inject"] 1 *})
   28.22    done
   28.23  
   28.24 @@ -228,11 +228,11 @@
   28.25           --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
   28.26    apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use])
   28.27    apply (case_tac "arg (ch w p)")
   28.28 -   apply (tactic {* action_simp_tac (simpset () addsimps [thm "Read_def",
   28.29 +   apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "Read_def",
   28.30       temp_rewrite (thm "enabled_ex")]) [thm "ReadInner_enabled", exI] [] 1 *})
   28.31     apply (force dest: base_pair [temp_use])
   28.32    apply (erule contrapos_np)
   28.33 -  apply (tactic {* action_simp_tac (simpset () addsimps [thm "Write_def",
   28.34 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "Write_def",
   28.35      temp_rewrite (thm "enabled_ex")])
   28.36      [thm "WriteInner_enabled", exI] [] 1 *})
   28.37    done
    29.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Wed Mar 19 22:47:39 2008 +0100
    29.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Wed Mar 19 22:50:42 2008 +0100
    29.3 @@ -220,9 +220,9 @@
    29.4    apply (rule historyI)
    29.5        apply assumption+
    29.6    apply (rule MI_base)
    29.7 -  apply (tactic {* action_simp_tac (simpset () addsimps [thm "HInit_def"]) [] [] 1 *})
    29.8 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "HInit_def"]) [] [] 1 *})
    29.9     apply (erule fun_cong)
   29.10 -  apply (tactic {* action_simp_tac (simpset () addsimps [thm "HNext_def"])
   29.11 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def"])
   29.12      [thm "busy_squareI"] [] 1 *})
   29.13    apply (erule fun_cong)
   29.14    done
   29.15 @@ -324,7 +324,7 @@
   29.16  
   29.17  lemma S1Hist: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S1 rmhist p)
   29.18           --> unchanged (rmhist!p)"
   29.19 -  by (tactic {* action_simp_tac (simpset () addsimps [thm "HNext_def", thm "S_def",
   29.20 +  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def", thm "S_def",
   29.21      thm "S1_def", thm "MemReturn_def", thm "RPCFail_def", thm "MClkReply_def",
   29.22      thm "Return_def"]) [] [temp_use (thm "squareE")] 1 *})
   29.23  
   29.24 @@ -340,7 +340,7 @@
   29.25  lemma S2Forward: "|- $(S2 rmhist p) & MClkFwd memCh crCh cst p
   29.26           & unchanged (e p, r p, m p, rmhist!p)
   29.27           --> (S3 rmhist p)$"
   29.28 -  by (tactic {* action_simp_tac (simpset () addsimps [thm "MClkFwd_def",
   29.29 +  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "MClkFwd_def",
   29.30      thm "Call_def", thm "e_def", thm "r_def", thm "m_def", thm "caller_def",
   29.31      thm "rtrner_def", thm "S_def", thm "S2_def", thm "S3_def", thm "Calling_def"]) [] [] 1 *})
   29.32  
   29.33 @@ -376,7 +376,7 @@
   29.34  lemma S3Forward: "|- RPCFwd crCh rmCh rst p & HNext rmhist p & $(S3 rmhist p)
   29.35           & unchanged (e p, c p, m p)
   29.36           --> (S4 rmhist p)$ & unchanged (rmhist!p)"
   29.37 -  by (tactic {* action_simp_tac (simpset () addsimps [thm "RPCFwd_def",
   29.38 +  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFwd_def",
   29.39      thm "HNext_def", thm "MemReturn_def", thm "RPCFail_def",
   29.40      thm "MClkReply_def", thm "Return_def", thm "Call_def", thm "e_def",
   29.41      thm "c_def", thm "m_def", thm "caller_def", thm "rtrner_def", thm "S_def",
   29.42 @@ -385,7 +385,7 @@
   29.43  lemma S3Fail: "|- RPCFail crCh rmCh rst p & $(S3 rmhist p) & HNext rmhist p
   29.44           & unchanged (e p, c p, m p)
   29.45           --> (S6 rmhist p)$"
   29.46 -  by (tactic {* action_simp_tac (simpset () addsimps [thm "HNext_def",
   29.47 +  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
   29.48      thm "RPCFail_def", thm "Return_def", thm "e_def", thm "c_def",
   29.49      thm "m_def", thm "caller_def", thm "rtrner_def", thm "MVOKBARF_def",
   29.50      thm "S_def", thm "S3_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
   29.51 @@ -412,7 +412,7 @@
   29.52  lemma S4ReadInner: "|- ReadInner rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
   29.53           & HNext rmhist p & $(MemInv mm l)
   29.54           --> (S4 rmhist p)$ & unchanged (rmhist!p)"
   29.55 -  by (tactic {* action_simp_tac (simpset () addsimps [thm "ReadInner_def",
   29.56 +  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "ReadInner_def",
   29.57      thm "GoodRead_def", thm "BadRead_def", thm "HNext_def", thm "MemReturn_def",
   29.58      thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "e_def",
   29.59      thm "c_def", thm "r_def", thm "rtrner_def", thm "caller_def",
   29.60 @@ -426,7 +426,7 @@
   29.61  
   29.62  lemma S4WriteInner: "|- WriteInner rmCh mm ires p l v & $(S4 rmhist p) & unchanged (e p, c p, r p)           & HNext rmhist p
   29.63           --> (S4 rmhist p)$ & unchanged (rmhist!p)"
   29.64 -  by (tactic {* action_simp_tac (simpset () addsimps [thm "WriteInner_def",
   29.65 +  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "WriteInner_def",
   29.66      thm "GoodWrite_def", thm "BadWrite_def", thm "HNext_def", thm "MemReturn_def",
   29.67      thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "e_def",
   29.68      thm "c_def", thm "r_def", thm "rtrner_def", thm "caller_def", thm "MVNROKBA_def",
   29.69 @@ -465,14 +465,14 @@
   29.70  
   29.71  lemma S5Reply: "|- RPCReply crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
   29.72         --> (S6 rmhist p)$"
   29.73 -  by (tactic {* action_simp_tac (simpset () addsimps [thm "RPCReply_def",
   29.74 +  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCReply_def",
   29.75      thm "Return_def", thm "e_def", thm "c_def", thm "m_def", thm "MVOKBA_def",
   29.76      thm "MVOKBARF_def", thm "caller_def", thm "rtrner_def", thm "S_def",
   29.77      thm "S5_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
   29.78  
   29.79  lemma S5Fail: "|- RPCFail crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
   29.80           --> (S6 rmhist p)$"
   29.81 -  by (tactic {* action_simp_tac (simpset () addsimps [thm "RPCFail_def",
   29.82 +  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFail_def",
   29.83      thm "Return_def", thm "e_def", thm "c_def", thm "m_def",
   29.84      thm "MVOKBARF_def", thm "caller_def", thm "rtrner_def",
   29.85      thm "S_def", thm "S5_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
   29.86 @@ -498,7 +498,7 @@
   29.87  lemma S6Retry: "|- MClkRetry memCh crCh cst p & HNext rmhist p & $S6 rmhist p
   29.88           & unchanged (e p,r p,m p)
   29.89           --> (S3 rmhist p)$ & unchanged (rmhist!p)"
   29.90 -  by (tactic {* action_simp_tac (simpset () addsimps [thm "HNext_def",
   29.91 +  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
   29.92      thm "MClkReply_def", thm "MClkRetry_def", thm "Call_def", thm "Return_def",
   29.93      thm "e_def", thm "r_def", thm "m_def", thm "caller_def", thm "rtrner_def",
   29.94      thm "S_def", thm "S6_def", thm "S3_def", thm "Calling_def"]) [] [] 1 *})
   29.95 @@ -506,7 +506,7 @@
   29.96  lemma S6Reply: "|- MClkReply memCh crCh cst p & HNext rmhist p & $S6 rmhist p
   29.97           & unchanged (e p,r p,m p)
   29.98           --> (S1 rmhist p)$"
   29.99 -  by (tactic {* action_simp_tac (simpset () addsimps [thm "HNext_def",
  29.100 +  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
  29.101      thm "MemReturn_def", thm "RPCFail_def", thm "Return_def", thm "MClkReply_def",
  29.102      thm "e_def", thm "r_def", thm "m_def", thm "caller_def", thm "rtrner_def",
  29.103      thm "S_def", thm "S6_def", thm "S1_def", thm "Calling_def"]) [] [] 1 *})
  29.104 @@ -538,7 +538,7 @@
  29.105  lemma Step1_2_1: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
  29.106           & ~unchanged (e p, c p, r p, m p, rmhist!p)  & $S1 rmhist p
  29.107           --> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
  29.108 -  apply (tactic {* action_simp_tac (simpset() addsimps [thm "ImpNext_def"]) []
  29.109 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
  29.110        (map temp_elim [thm "S1ClerkUnch", thm "S1RPCUnch", thm "S1MemUnch", thm "S1Hist"]) 1 *})
  29.111     apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use (thm "S1Env")]) *})
  29.112    done
  29.113 @@ -547,7 +547,7 @@
  29.114           & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
  29.115           --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
  29.116               & unchanged (e p, r p, m p, rmhist!p)"
  29.117 -  apply (tactic {* action_simp_tac (simpset() addsimps [thm "ImpNext_def"]) []
  29.118 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
  29.119      (map temp_elim [thm "S2EnvUnch", thm "S2RPCUnch", thm "S2MemUnch", thm "S2Hist"]) 1 *})
  29.120     apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use (thm "S2Clerk"),
  29.121       temp_use (thm "S2Forward")]) *})
  29.122 @@ -557,9 +557,9 @@
  29.123           & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p
  29.124           --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p))
  29.125               | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
  29.126 -  apply (tactic {* action_simp_tac (simpset() addsimps [thm "ImpNext_def"]) []
  29.127 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
  29.128      (map temp_elim [thm "S3EnvUnch", thm "S3ClerkUnch", thm "S3MemUnch"]) 1 *})
  29.129 -  apply (tactic {* action_simp_tac (simpset()) []
  29.130 +  apply (tactic {* action_simp_tac @{simpset} []
  29.131      (thm "squareE" :: map temp_elim [thm "S3RPC", thm "S3Forward", thm "S3Fail"]) 1 *})
  29.132     apply (auto dest!: S3Hist [temp_use])
  29.133    done
  29.134 @@ -570,9 +570,9 @@
  29.135           --> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p))
  29.136               | ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p))
  29.137               | ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"
  29.138 -  apply (tactic {* action_simp_tac (simpset() addsimps [thm "ImpNext_def"]) []
  29.139 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
  29.140      (map temp_elim [thm "S4EnvUnch", thm "S4ClerkUnch", thm "S4RPCUnch"]) 1 *})
  29.141 -  apply (tactic {* action_simp_tac (simpset() addsimps [thm "RNext_def"]) []
  29.142 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "RNext_def"]) []
  29.143      (thm "squareE" :: map temp_elim [thm "S4Read", thm "S4Write", thm "S4Return"]) 1 *})
  29.144    apply (auto dest!: S4Hist [temp_use])
  29.145    done
  29.146 @@ -581,9 +581,9 @@
  29.147                & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p
  29.148           --> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p))
  29.149               | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
  29.150 -  apply (tactic {* action_simp_tac (simpset() addsimps [thm "ImpNext_def"]) []
  29.151 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
  29.152      (map temp_elim [thm "S5EnvUnch", thm "S5ClerkUnch", thm "S5MemUnch", thm "S5Hist"]) 1 *})
  29.153 -  apply (tactic {* action_simp_tac (simpset()) [] [thm "squareE", temp_elim (thm "S5RPC")] 1 *})
  29.154 +  apply (tactic {* action_simp_tac @{simpset} [] [thm "squareE", temp_elim (thm "S5RPC")] 1 *})
  29.155     apply (tactic {* auto_tac (MI_fast_css addSDs2
  29.156       [temp_use (thm "S5Reply"), temp_use (thm "S5Fail")]) *})
  29.157    done
  29.158 @@ -592,9 +592,9 @@
  29.159                & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p
  29.160           --> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))
  29.161               | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
  29.162 -  apply (tactic {* action_simp_tac (simpset() addsimps [thm "ImpNext_def"]) []
  29.163 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
  29.164      (map temp_elim [thm "S6EnvUnch", thm "S6RPCUnch", thm "S6MemUnch"]) 1 *})
  29.165 -  apply (tactic {* action_simp_tac (simpset()) []
  29.166 +  apply (tactic {* action_simp_tac @{simpset} []
  29.167      (thm "squareE" :: map temp_elim [thm "S6Clerk", thm "S6Retry", thm "S6Reply"]) 1 *})
  29.168       apply (auto dest: S6Hist [temp_use])
  29.169    done
  29.170 @@ -606,7 +606,7 @@
  29.171  section "Initialization (Step 1.3)"
  29.172  
  29.173  lemma Step1_3: "|- S1 rmhist p --> PInit (resbar rmhist) p"
  29.174 -  by (tactic {* action_simp_tac (simpset () addsimps [thm "resbar_def",
  29.175 +  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "resbar_def",
  29.176      thm "PInit_def", thm "S_def", thm "S1_def"]) [] [] 1 *})
  29.177  
  29.178  (* ----------------------------------------------------------------------
  29.179 @@ -625,7 +625,7 @@
  29.180           & unchanged (e p, r p, m p, rmhist!p)
  29.181           --> unchanged (rtrner memCh!p, resbar rmhist!p)"
  29.182    by (tactic {* action_simp_tac
  29.183 -    (simpset() addsimps [thm "MClkFwd_def", thm "e_def", thm "r_def", thm "m_def",
  29.184 +    (@{simpset} addsimps [thm "MClkFwd_def", thm "e_def", thm "r_def", thm "m_def",
  29.185      thm "resbar_def", thm "S_def", thm "S2_def", thm "S3_def"]) [] [] 1 *})
  29.186  
  29.187  lemma Step1_4_3a: "|- RPCFwd crCh rmCh rst p & $S3 rmhist p & (S4 rmhist p)$
  29.188 @@ -633,7 +633,7 @@
  29.189           --> unchanged (rtrner memCh!p, resbar rmhist!p)"
  29.190    apply clarsimp
  29.191    apply (drule S3_excl [temp_use] S4_excl [temp_use])+
  29.192 -  apply (tactic {* action_simp_tac (simpset () addsimps [thm "e_def",
  29.193 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
  29.194      thm "c_def", thm "m_def", thm "resbar_def", thm "S_def", thm "S3_def"]) [] [] 1 *})
  29.195    done
  29.196  
  29.197 @@ -652,11 +652,11 @@
  29.198           --> ReadInner memCh mm (resbar rmhist) p l"
  29.199    apply clarsimp
  29.200    apply (drule S4_excl [temp_use])+
  29.201 -  apply (tactic {* action_simp_tac (simpset () addsimps [thm "ReadInner_def",
  29.202 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ReadInner_def",
  29.203      thm "GoodRead_def", thm "BadRead_def", thm "e_def", thm "c_def", thm "m_def"]) [] [] 1 *})
  29.204       apply (auto simp: resbar_def)
  29.205         apply (tactic {* ALLGOALS (action_simp_tac
  29.206 -                (simpset() addsimps [thm "RPCRelayArg_def", thm "MClkRelayArg_def",
  29.207 +                (@{simpset} addsimps [thm "RPCRelayArg_def", thm "MClkRelayArg_def",
  29.208                    thm "S_def", thm "S4_def", thm "RdRequest_def", thm "MemInv_def"])
  29.209                  [] [thm "impE", thm "MemValNotAResultE"]) *})
  29.210    done
  29.211 @@ -671,11 +671,11 @@
  29.212           --> WriteInner memCh mm (resbar rmhist) p l v"
  29.213    apply clarsimp
  29.214    apply (drule S4_excl [temp_use])+
  29.215 -  apply (tactic {* action_simp_tac (simpset () addsimps
  29.216 +  apply (tactic {* action_simp_tac (@{simpset} addsimps
  29.217      [thm "WriteInner_def", thm "GoodWrite_def", thm "BadWrite_def", thm "e_def",
  29.218      thm "c_def", thm "m_def"]) [] [] 1 *})
  29.219       apply (auto simp: resbar_def)
  29.220 -    apply (tactic {* ALLGOALS (action_simp_tac (simpset () addsimps
  29.221 +    apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
  29.222        [thm "RPCRelayArg_def", thm "MClkRelayArg_def", thm "S_def",
  29.223        thm "S4_def", thm "WrRequest_def"]) [] []) *})
  29.224    done
  29.225 @@ -688,7 +688,7 @@
  29.226  lemma Step1_4_4c: "|- MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$
  29.227           & unchanged (e p, c p, r p)
  29.228           --> unchanged (rtrner memCh!p, resbar rmhist!p)"
  29.229 -  apply (tactic {* action_simp_tac (simpset () addsimps [thm "e_def",
  29.230 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
  29.231      thm "c_def", thm "r_def", thm "resbar_def"]) [] [] 1 *})
  29.232    apply (drule S4_excl [temp_use] S5_excl [temp_use])+
  29.233    apply (tactic {* auto_tac (MI_fast_css addsimps2 [thm "MemReturn_def", thm "Return_def"]) *})
  29.234 @@ -717,11 +717,11 @@
  29.235           --> MemReturn memCh (resbar rmhist) p"
  29.236    apply clarsimp
  29.237    apply (drule S6_excl [temp_use])+
  29.238 -  apply (tactic {* action_simp_tac (simpset () addsimps [thm "e_def",
  29.239 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
  29.240      thm "r_def", thm "m_def", thm "MClkReply_def", thm "MemReturn_def",
  29.241      thm "Return_def", thm "resbar_def"]) [] [] 1 *})
  29.242      apply simp_all (* simplify if-then-else *)
  29.243 -    apply (tactic {* ALLGOALS (action_simp_tac (simpset () addsimps
  29.244 +    apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
  29.245        [thm "MClkReplyVal_def", thm "S6_def", thm "S_def"]) [] [thm "MVOKBARFnotNR"]) *})
  29.246    done
  29.247  
  29.248 @@ -730,7 +730,7 @@
  29.249           --> MemFail memCh (resbar rmhist) p"
  29.250    apply clarsimp
  29.251    apply (drule S3_excl [temp_use])+
  29.252 -  apply (tactic {* action_simp_tac (simpset () addsimps [thm "e_def", thm "r_def",
  29.253 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def", thm "r_def",
  29.254      thm "m_def", thm "MClkRetry_def", thm "MemFail_def", thm "resbar_def"]) [] [] 1 *})
  29.255     apply (auto simp: S6_def S_def)
  29.256    done
  29.257 @@ -862,14 +862,14 @@
  29.258  
  29.259  lemma S1_RNextdisabled: "|- S1 rmhist p -->
  29.260           ~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
  29.261 -  apply (tactic {* action_simp_tac (simpset () addsimps [thm "angle_def",
  29.262 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def",
  29.263      thm "S_def", thm "S1_def"]) [notI] [thm "enabledE", temp_elim (thm "Memoryidle")] 1 *})
  29.264    apply force
  29.265    done
  29.266  
  29.267  lemma S1_Returndisabled: "|- S1 rmhist p -->
  29.268           ~Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
  29.269 -  by (tactic {* action_simp_tac (simpset () addsimps [thm "angle_def", thm "MemReturn_def",
  29.270 +  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def", thm "MemReturn_def",
  29.271      thm "Return_def", thm "S_def", thm "S1_def"]) [notI] [thm "enabledE"] 1 *})
  29.272  
  29.273  lemma RNext_fair: "|- []<>S1 rmhist p
  29.274 @@ -1048,7 +1048,7 @@
  29.275  
  29.276  lemma MClkReplyS6:
  29.277    "|- $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) --> $S6 rmhist p"
  29.278 -  by (tactic {* action_simp_tac (simpset () addsimps [thm "angle_def",
  29.279 +  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def",
  29.280      thm "MClkReply_def", thm "Return_def", thm "ImpInv_def", thm "S_def",
  29.281      thm "S1_def", thm "S2_def", thm "S3_def", thm "S4_def", thm "S5_def"]) [] [] 1 *})
  29.282  
  29.283 @@ -1056,7 +1056,7 @@
  29.284    apply (auto simp: c_def intro!: MClkReply_enabled [temp_use])
  29.285       apply (cut_tac MI_base)
  29.286       apply (blast dest: base_pair)
  29.287 -    apply (tactic {* ALLGOALS (action_simp_tac (simpset ()
  29.288 +    apply (tactic {* ALLGOALS (action_simp_tac (@{simpset}
  29.289        addsimps [thm "S_def", thm "S6_def"]) [] []) *})
  29.290    done
  29.291  
  29.292 @@ -1067,7 +1067,7 @@
  29.293    apply (subgoal_tac "sigma |= []<> (<MClkReply memCh crCh cst p>_ (c p))")
  29.294     apply (erule InfiniteEnsures)
  29.295      apply assumption
  29.296 -   apply (tactic {* action_simp_tac (simpset()) []
  29.297 +   apply (tactic {* action_simp_tac @{simpset} []
  29.298       (map temp_elim [thm "MClkReplyS6", thm "S6MClkReply_successors"]) 1 *})
  29.299    apply (auto simp: SF_def)
  29.300    apply (erule contrapos_np)
  29.301 @@ -1154,7 +1154,7 @@
  29.302           sigma |= []<>S6 rmhist p --> []<>S1 rmhist p |]
  29.303        ==> sigma |= []<>S1 rmhist p"
  29.304    apply (rule classical)
  29.305 -  apply (tactic {* asm_lr_simp_tac (simpset() addsimps
  29.306 +  apply (tactic {* asm_lr_simp_tac (@{simpset} addsimps
  29.307      [temp_use (thm "NotBox"), temp_rewrite (thm "NotDmd")]) 1 *})
  29.308    apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use])
  29.309    done
    30.1 --- a/src/HOL/TLA/Memory/RPC.thy	Wed Mar 19 22:47:39 2008 +0100
    30.2 +++ b/src/HOL/TLA/Memory/RPC.thy	Wed Mar 19 22:50:42 2008 +0100
    30.3 @@ -103,14 +103,14 @@
    30.4  (* Enabledness of some actions *)
    30.5  lemma RPCFail_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
    30.6      |- ~Calling rcv p & Calling send p --> Enabled (RPCFail send rcv rst p)"
    30.7 -  by (tactic {* action_simp_tac (simpset () addsimps [thm "RPCFail_def",
    30.8 +  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFail_def",
    30.9      thm "Return_def", thm "caller_def", thm "rtrner_def"]) [exI]
   30.10      [thm "base_enabled", thm "Pair_inject"] 1 *})
   30.11  
   30.12  lemma RPCReply_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
   30.13        |- ~Calling rcv p & Calling send p & rst!p = #rpcB  
   30.14           --> Enabled (RPCReply send rcv rst p)"
   30.15 -  by (tactic {* action_simp_tac (simpset () addsimps [thm "RPCReply_def",
   30.16 +  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCReply_def",
   30.17      thm "Return_def", thm "caller_def", thm "rtrner_def"]) [exI]
   30.18      [thm "base_enabled", thm "Pair_inject"] 1 *})
   30.19  
    31.1 --- a/src/HOL/W0/W0.thy	Wed Mar 19 22:47:39 2008 +0100
    31.2 +++ b/src/HOL/W0/W0.thy	Wed Mar 19 22:50:42 2008 +0100
    31.3 @@ -196,15 +196,15 @@
    31.4    apply (unfold new_tv_def)
    31.5    apply (tactic "safe_tac HOL_cs")
    31.6    -- {* @{text \<Longrightarrow>} *}
    31.7 -    apply (tactic {* fast_tac (HOL_cs addDs [@{thm leD}] addss (simpset()
    31.8 +    apply (tactic {* fast_tac (HOL_cs addDs [@{thm leD}] addss (@{simpset}
    31.9        addsimps [thm "free_tv_subst", thm "dom_def"])) 1 *})
   31.10     apply (subgoal_tac "m \<in> cod s \<or> s l = TVar l")
   31.11      apply (tactic "safe_tac HOL_cs")
   31.12 -     apply (tactic {* fast_tac (HOL_cs addDs [UnI2] addss (simpset()
   31.13 +     apply (tactic {* fast_tac (HOL_cs addDs [UnI2] addss (@{simpset}
   31.14         addsimps [thm "free_tv_subst"])) 1 *})
   31.15      apply (drule_tac P = "\<lambda>x. m \<in> free_tv x" in subst, assumption)
   31.16      apply simp
   31.17 -   apply (tactic {* fast_tac (set_cs addss (simpset()
   31.18 +   apply (tactic {* fast_tac (set_cs addss (@{simpset}
   31.19       addsimps [thm "free_tv_subst", thm "cod_def", thm "dom_def"])) 1 *})
   31.20    -- {* @{text \<Longleftarrow>} *}
   31.21    apply (unfold free_tv_subst cod_def dom_def)
   31.22 @@ -350,7 +350,7 @@
   31.23    apply (tactic {*
   31.24      fast_tac (set_cs addSDs [thm "free_tv_app_subst_te" RS subsetD,
   31.25      thm "free_tv_subst_var" RS subsetD]
   31.26 -    addss (simpset() delsimps (thms "bex_simps")
   31.27 +    addss (@{simpset} delsimps (thms "bex_simps")
   31.28      addsimps [thm "cod_def", thm "dom_def"])) 1 *})
   31.29    done
   31.30  
   31.31 @@ -555,7 +555,7 @@
   31.32        new_tv_le)
   31.33     apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
   31.34       addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
   31.35 -     addss (simpset())) 1 *})
   31.36 +     addss @{simpset}) 1 *})
   31.37    apply (rule lessI [THEN new_tv_subst_var])
   31.38    apply (erule sym [THEN mgu_new])
   31.39      apply (bestsimp intro!: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te
   31.40 @@ -563,7 +563,7 @@
   31.41          lessI [THEN less_imp_le, THEN new_tv_subst_le] new_tv_le)
   31.42    apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
   31.43      addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
   31.44 -    addss (simpset())) 1 *})
   31.45 +    addss @{simpset}) 1 *})
   31.46    done
   31.47  
   31.48  lemma free_tv_W: "!!n a s t m v. \<W> e a n = Ok (s, t, m) \<Longrightarrow>
   31.49 @@ -616,7 +616,7 @@
   31.50      thm "free_tv_subst_var" RS subsetD,
   31.51      thm "free_tv_app_subst_te" RS subsetD,
   31.52      thm "free_tv_app_subst_tel" RS subsetD, @{thm less_le_trans}, subsetD]
   31.53 -    addSEs [UnE] addss (simpset() setSolver unsafe_solver)) 1 *})
   31.54 +    addSEs [UnE] addss (@{simpset} setSolver unsafe_solver)) 1 *})
   31.55        -- {* builtin arithmetic in simpset messes things up *}
   31.56    done
   31.57  
   31.58 @@ -798,7 +798,7 @@
   31.59      apply (simp add: app_subst_list split: split_if)
   31.60     txt {* case @{text "Abs e"} *}
   31.61     apply (tactic {* asm_full_simp_tac
   31.62 -     (simpset() setloop (split_inside_tac [thm "split_bind"])) 1 *})
   31.63 +     (@{simpset} setloop (split_inside_tac [thm "split_bind"])) 1 *})
   31.64     apply (intro strip)
   31.65     apply (rule conjI)
   31.66      apply (intro strip)
   31.67 @@ -814,7 +814,7 @@
   31.68     apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp,
   31.69       thm "new_tv_subst_le", @{thm less_imp_le}, @{thm lessI}]) 1 *})
   31.70    txt {* case @{text "App e1 e2"} *}
   31.71 -  apply (tactic {* simp_tac (simpset () setloop (split_inside_tac [thm "split_bind"])) 1 *})
   31.72 +  apply (tactic {* simp_tac (@{simpset} setloop (split_inside_tac [thm "split_bind"])) 1 *})
   31.73    apply (intro strip)
   31.74    apply (rename_tac s1' t1 n1 s2' t2 n2 sa)
   31.75    apply (rule conjI)
    32.1 --- a/src/HOLCF/IOA/ABP/Correctness.thy	Wed Mar 19 22:47:39 2008 +0100
    32.2 +++ b/src/HOLCF/IOA/ABP/Correctness.thy	Wed Mar 19 22:50:42 2008 +0100
    32.3 @@ -82,7 +82,7 @@
    32.4  lemma last_ind_on_first:
    32.5      "l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))"
    32.6    apply simp
    32.7 -  apply (tactic {* auto_tac (claset(),
    32.8 +  apply (tactic {* auto_tac (@{claset},
    32.9      HOL_ss addsplits [thm"list.split"]
   32.10      addsimps (thms "reverse.simps" @ [thm "hd_append", thm "rev_red_not_nil"])) *})
   32.11    done
    33.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Mar 19 22:47:39 2008 +0100
    33.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Mar 19 22:50:42 2008 +0100
    33.3 @@ -6,7 +6,7 @@
    33.4  Proof generator for domain command.
    33.5  *)
    33.6  
    33.7 -val HOLCF_ss = simpset();
    33.8 +val HOLCF_ss = @{simpset};
    33.9  
   33.10  structure Domain_Theorems = struct
   33.11  
   33.12 @@ -113,7 +113,7 @@
   33.13  
   33.14  val dist_eqI = prove_goal (the_context ()) "!!x::'a::po. ~ x << y ==> x ~= y" 
   33.15    (fn prems =>
   33.16 -    [blast_tac (claset () addDs [antisym_less_inverse]) 1]);
   33.17 +    [blast_tac (@{claset} addDs [antisym_less_inverse]) 1]);
   33.18  
   33.19  in
   33.20  
   33.21 @@ -638,7 +638,7 @@
   33.22  (* ----- theorems concerning finite approximation and finite induction ------ *)
   33.23  
   33.24  local
   33.25 -  val iterate_Cprod_ss = simpset_of (theory "Fix");
   33.26 +  val iterate_Cprod_ss = simpset_of @{theory Fix};
   33.27    val copy_con_rews  = copy_rews @ con_rews;
   33.28    val copy_take_defs =
   33.29      (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;