1.1 --- a/src/CCL/Type.thy	Sat Jul 21 17:40:40 2007 +0200
     1.2 +++ b/src/CCL/Type.thy	Sat Jul 21 23:25:00 2007 +0200
     1.3 @@ -130,15 +130,15 @@
     1.4    val bexE = thm "bexE"
     1.5  in
     1.6  
     1.7 -  fun mk_ncanT_tac thy defs top_crls crls s = prove_goalw thy defs s
     1.8 +  fun mk_ncanT_tac ctxt defs top_crls crls s = prove_goalw (ProofContext.theory_of ctxt) defs s
     1.9      (fn major::prems => [(resolve_tac ([major] RL top_crls) 1),
    1.10                           (REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))),
    1.11 -                         (ALLGOALS (asm_simp_tac (simpset ()))),
    1.12 +                         (ALLGOALS (asm_simp_tac (local_simpset_of ctxt))),
    1.13                           (ALLGOALS (ares_tac (prems RL [lemma]) ORELSE'
    1.14                                      etac bspec )),
    1.15 -                         (safe_tac (claset () addSIs prems))])
    1.16 +                         (safe_tac (local_claset_of ctxt addSIs prems))])
    1.17  
    1.18 -  val ncanT_tac = mk_ncanT_tac (the_context ()) [] case_rls case_rls
    1.19 +  val ncanT_tac = mk_ncanT_tac @{context} [] case_rls case_rls
    1.20  end
    1.21  *}
    1.22  
    1.23 @@ -275,7 +275,7 @@
    1.24  lemmas icanTs = zeroT succT nilT consT
    1.25  
    1.26  ML {*
    1.27 -val incanT_tac = mk_ncanT_tac (the_context ()) [] (thms "icase_rls") (thms "case_rls");
    1.28 +val incanT_tac = mk_ncanT_tac @{context} [] (thms "icase_rls") (thms "case_rls");
    1.29  
    1.30  bind_thm ("ncaseT", incanT_tac
    1.31    "[| n:Nat; n=zero ==> b:C(zero); !!x.[| x:Nat;  n=succ(x) |] ==> c(x):C(succ(x)) |] ==> ncase(n,b,c) : C(n)");
    1.32 @@ -469,18 +469,18 @@
    1.33     "[| <h,h'> : lfp(%x. EQgen(x) Un R Un EQ); <t,t'> : lfp(%x. EQgen(x) Un R Un EQ) |] ==> <h$t,h'$t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"];
    1.34  
    1.35  fun EQgen_raw_tac i =
    1.36 -  (REPEAT (resolve_tac (EQgenIs @ [thm "EQ_refl" RS (thm "EQgen_mono" RS ci3_AI)] @
    1.37 -    (EQgenIs RL [thm "EQgen_mono" RS ci3_AgenI]) @ [thm "EQgen_mono" RS ci3_RI]) i))
    1.38 +  (REPEAT (resolve_tac (EQgenIs @ [@{thm EQ_refl} RS (@{thm EQgen_mono} RS ci3_AI)] @
    1.39 +    (EQgenIs RL [@{thm EQgen_mono} RS ci3_AgenI]) @ [@{thm EQgen_mono} RS ci3_RI]) i))
    1.40  
    1.41  (* Goals of the form R <= EQgen(R) - rewrite elements <a,b> : EQgen(R) using rews and *)
    1.42  (* then reduce this to a goal <a',b'> : R (hopefully?)                                *)
    1.43  (*      rews are rewrite rules that would cause looping in the simpifier              *)
    1.44  
    1.45 -fun EQgen_tac simp_set rews i =
    1.46 +fun EQgen_tac ctxt rews i =
    1.47   SELECT_GOAL
    1.48 -   (TRY (CLASET safe_tac) THEN
    1.49 -    resolve_tac ((rews@[refl]) RL ((rews@[refl]) RL [thm "ssubst_pair"])) i THEN
    1.50 -    ALLGOALS (simp_tac simp_set) THEN
    1.51 +   (TRY (safe_tac (local_claset_of ctxt)) THEN
    1.52 +    resolve_tac ((rews@[refl]) RL ((rews@[refl]) RL [@{thm ssubst_pair}])) i THEN
    1.53 +    ALLGOALS (simp_tac (local_simpset_of ctxt)) THEN
    1.54      ALLGOALS EQgen_raw_tac) i
    1.55  *}
    1.56  

     2.1 --- a/src/CCL/ex/Flag.thy	Sat Jul 21 17:40:40 2007 +0200
     2.2 +++ b/src/CCL/ex/Flag.thy	Sat Jul 21 23:25:00 2007 +0200
     2.3 @@ -56,7 +56,7 @@
     2.4    unfolding ColourXH by blast+
     2.5  
     2.6  ML {*
     2.7 -bind_thm ("ccaseT", mk_ncanT_tac (the_context ())
     2.8 +bind_thm ("ccaseT", mk_ncanT_tac @{context}
     2.9    (thms "flag_defs") (thms "case_rls") (thms "case_rls")
    2.10    "[| c:Colour; c=red ==> r : C(red); c=white ==> w : C(white); c=blue ==> b : C(blue) |] ==> ccase(c,r,w,b) : C(c)");
    2.11  *}

     3.1 --- a/src/CCL/ex/Stream.thy	Sat Jul 21 17:40:40 2007 +0200
     3.2 +++ b/src/CCL/ex/Stream.thy	Sat Jul 21 23:25:00 2007 +0200
     3.3 @@ -37,7 +37,7 @@
     3.4     apply (blast intro: 1)
     3.5    apply safe
     3.6    apply (drule ListsXH [THEN iffD1])
     3.7 -  apply (tactic "EQgen_tac (simpset ()) [] 1")
     3.8 +  apply (tactic "EQgen_tac @{context} [] 1")
     3.9     apply fastsimp
    3.10    done
    3.11  
    3.12 @@ -51,7 +51,7 @@
    3.13    apply (blast intro: 1)
    3.14    apply safe
    3.15    apply (drule ListsXH [THEN iffD1])
    3.16 -  apply (tactic "EQgen_tac (simpset ()) [] 1")
    3.17 +  apply (tactic "EQgen_tac @{context} [] 1")
    3.18    apply blast
    3.19    done
    3.20  
    3.21 @@ -67,9 +67,9 @@
    3.22    apply (blast intro: prems)
    3.23    apply safe
    3.24    apply (drule ListsXH [THEN iffD1])
    3.25 -  apply (tactic "EQgen_tac (simpset ()) [] 1")
    3.26 +  apply (tactic "EQgen_tac @{context} [] 1")
    3.27    apply (drule ListsXH [THEN iffD1])
    3.28 -  apply (tactic "EQgen_tac (simpset ()) [] 1")
    3.29 +  apply (tactic "EQgen_tac @{context} [] 1")
    3.30    apply blast
    3.31    done
    3.32  
    3.33 @@ -86,11 +86,11 @@
    3.34    apply (blast intro: prems)
    3.35    apply safe
    3.36    apply (drule ListsXH [THEN iffD1])
    3.37 -  apply (tactic "EQgen_tac (simpset ()) [] 1")
    3.38 +  apply (tactic "EQgen_tac @{context} [] 1")
    3.39     prefer 2
    3.40     apply blast
    3.41    apply (tactic {* DEPTH_SOLVE (etac (XH_to_E (thm "ListsXH")) 1
    3.42 -    THEN EQgen_tac (simpset ()) [] 1) *})
    3.43 +    THEN EQgen_tac @{context} [] 1) *})
    3.44    done
    3.45  
    3.46  
    3.47 @@ -104,7 +104,7 @@
    3.48    apply (blast intro: prems)
    3.49    apply safe
    3.50    apply (drule IListsXH [THEN iffD1])
    3.51 -  apply (tactic "EQgen_tac (simpset ()) [] 1")
    3.52 +  apply (tactic "EQgen_tac @{context} [] 1")
    3.53    apply blast
    3.54    done
    3.55  
    3.56 @@ -136,7 +136,7 @@
    3.57    apply (tactic {* eq_coinduct3_tac
    3.58      "{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}" 1*})
    3.59    apply (fast intro!: napplyBzero [symmetric] napplyBzero [symmetric, THEN arg_cong])
    3.60 -  apply (tactic {* EQgen_tac (simpset ()) [thm "iter1B", thm "iter2Blemma"] 1 *})
    3.61 +  apply (tactic {* EQgen_tac @{context} [thm "iter1B", thm "iter2Blemma"] 1 *})
    3.62    apply (subst napply_f, assumption)
    3.63    apply (rule_tac f1 = f in napplyBsucc [THEN subst])
    3.64    apply blast

     4.1 --- a/src/HOL/Algebra/abstract/Ideal2.thy	Sat Jul 21 17:40:40 2007 +0200
     4.2 +++ b/src/HOL/Algebra/abstract/Ideal2.thy	Sat Jul 21 23:25:00 2007 +0200
     4.3 @@ -275,7 +275,7 @@
     4.4    apply (unfold prime_def)
     4.5    apply (rule conjI)
     4.6     apply (rule_tac [2] conjI)
     4.7 -    apply (tactic "Clarify_tac 3")
     4.8 +    apply (tactic "clarify_tac @{claset} 3")
     4.9      apply (drule_tac [3] I = "ideal_of {a, b}" and x = "1" in irred_imp_max_ideal)
    4.10        apply (auto intro: ideal_of_is_ideal pid_ax simp add: irred_def not_dvd_psubideal pid_ax)
    4.11    apply (simp add: ideal_of_2_structure)

     5.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Sat Jul 21 17:40:40 2007 +0200
     5.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Sat Jul 21 23:25:00 2007 +0200
     5.3 @@ -495,7 +495,7 @@
     5.4  (* fields are integral domains *)
     5.5  
     5.6  lemma field_integral: "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0"
     5.7 -  apply (tactic "Step_tac 1")
     5.8 +  apply (tactic "step_tac @{claset} 1")
     5.9    apply (rule_tac a = " (a*b) * inverse b" in box_equals)
    5.10      apply (rule_tac [3] refl)
    5.11     prefer 2

     6.1 --- a/src/HOL/Auth/Public.thy	Sat Jul 21 17:40:40 2007 +0200
     6.2 +++ b/src/HOL/Auth/Public.thy	Sat Jul 21 23:25:00 2007 +0200
     6.3 @@ -425,31 +425,31 @@
     6.4  
     6.5  ML
     6.6  {*
     6.7 -val Nonce_supply = thm "Nonce_supply";
     6.8 -
     6.9 -(*Tactic for possibility theorems (Isar interface)*)
    6.10 -fun gen_possibility_tac ss state = state |>
    6.11 +(*Tactic for possibility theorems*)
    6.12 +fun possibility_tac ctxt =
    6.13      REPEAT (*omit used_Says so that Nonces start from different traces!*)
    6.14 -    (ALLGOALS (simp_tac (ss delsimps [used_Says]))
    6.15 +    (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says]))
    6.16       THEN
    6.17       REPEAT_FIRST (eq_assume_tac ORELSE' 
    6.18 -                   resolve_tac [refl, conjI, Nonce_supply]))
    6.19 -
    6.20 -(*Tactic for possibility theorems (ML script version)*)
    6.21 -fun possibility_tac state = gen_possibility_tac (simpset()) state
    6.22 +                   resolve_tac [refl, conjI, @{thm Nonce_supply}]))
    6.23  
    6.24  (*For harder protocols (such as Recur) where we have to set up some
    6.25    nonces and keys initially*)
    6.26 -fun basic_possibility_tac st = st |>
    6.27 +fun basic_possibility_tac ctxt =
    6.28      REPEAT 
    6.29 -    (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
    6.30 +    (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
    6.31       THEN
    6.32       REPEAT_FIRST (resolve_tac [refl, conjI]))
    6.33  *}
    6.34  
    6.35  method_setup possibility = {*
    6.36      Method.ctxt_args (fn ctxt =>
    6.37 -        Method.SIMPLE_METHOD (gen_possibility_tac (local_simpset_of ctxt))) *}
    6.38 +        Method.SIMPLE_METHOD (possibility_tac ctxt)) *}
    6.39 +    "for proving possibility theorems"
    6.40 +
    6.41 +method_setup basic_possibility = {*
    6.42 +    Method.ctxt_args (fn ctxt =>
    6.43 +        Method.SIMPLE_METHOD (basic_possibility_tac ctxt)) *}
    6.44      "for proving possibility theorems"
    6.45  
    6.46  end

     7.1 --- a/src/HOL/Auth/Recur.thy	Sat Jul 21 17:40:40 2007 +0200
     7.2 +++ b/src/HOL/Auth/Recur.thy	Sat Jul 21 23:25:00 2007 +0200
     7.3 @@ -163,7 +163,7 @@
     7.4                            [OF _ _ respond.One 
     7.5                                    [THEN respond.Cons, THEN respond.Cons]],
     7.6                       THEN recur.RA4, THEN recur.RA4])
     7.7 -apply (tactic "basic_possibility_tac")
     7.8 +apply basic_possibility
     7.9  apply (tactic "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1)")
    7.10  done
    7.11  

     8.1 --- a/src/HOL/Auth/Shared.thy	Sat Jul 21 17:40:40 2007 +0200
     8.2 +++ b/src/HOL/Auth/Shared.thy	Sat Jul 21 23:25:00 2007 +0200
     8.3 @@ -195,22 +195,19 @@
     8.4  {*
     8.5  (*Omitting used_Says makes the tactic much faster: it leaves expressions
     8.6      such as  Nonce ?N \<notin> used evs that match Nonce_supply*)
     8.7 -fun gen_possibility_tac ss state = state |>
     8.8 +fun possibility_tac ctxt =
     8.9     (REPEAT 
    8.10 -    (ALLGOALS (simp_tac (ss delsimps [used_Says, used_Notes, used_Gets] 
    8.11 +    (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says, used_Notes, used_Gets] 
    8.12                           setSolver safe_solver))
    8.13       THEN
    8.14       REPEAT_FIRST (eq_assume_tac ORELSE' 
    8.15                     resolve_tac [refl, conjI, Nonce_supply])))
    8.16  
    8.17 -(*Tactic for possibility theorems (ML script version)*)
    8.18 -fun possibility_tac state = gen_possibility_tac (simpset()) state
    8.19 -
    8.20  (*For harder protocols (such as Recur) where we have to set up some
    8.21    nonces and keys initially*)
    8.22 -fun basic_possibility_tac st = st |>
    8.23 +fun basic_possibility_tac ctxt =
    8.24      REPEAT 
    8.25 -    (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
    8.26 +    (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
    8.27       THEN
    8.28       REPEAT_FIRST (resolve_tac [refl, conjI]))
    8.29  *}
    8.30 @@ -273,10 +270,15 @@
    8.31  
    8.32  method_setup possibility = {*
    8.33      Method.ctxt_args (fn ctxt =>
    8.34 -        Method.SIMPLE_METHOD (gen_possibility_tac (local_simpset_of ctxt))) *}
    8.35 +        Method.SIMPLE_METHOD (possibility_tac ctxt)) *}
    8.36 +    "for proving possibility theorems"
    8.37 +
    8.38 +method_setup basic_possibility = {*
    8.39 +    Method.ctxt_args (fn ctxt =>
    8.40 +        Method.SIMPLE_METHOD (basic_possibility_tac ctxt)) *}
    8.41      "for proving possibility theorems"
    8.42  
    8.43  lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
    8.44 -by (induct e, auto simp: knows_Cons)
    8.45 +by (induct e) (auto simp: knows_Cons)
    8.46  
    8.47  end

     9.1 --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Sat Jul 21 17:40:40 2007 +0200
     9.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Sat Jul 21 23:25:00 2007 +0200
     9.3 @@ -756,13 +756,13 @@
     9.4   (*SR11*)  forward_tac [Outpts_A_Card_form_10] 21 THEN
     9.5             eresolve_tac [exE] 22 THEN eresolve_tac [exE] 22
     9.6  
     9.7 -val parts_prepare_tac = 
     9.8 +fun parts_prepare_tac ctxt = 
     9.9             prepare_tac THEN
    9.10   (*SR9*)   dresolve_tac [Gets_imp_knows_Spy_parts_Snd] 18 THEN 
    9.11   (*SR9*)   dresolve_tac [Gets_imp_knows_Spy_parts_Snd] 19 THEN 
    9.12   (*Oops1*) dresolve_tac [Outpts_B_Card_form_7] 25    THEN               
    9.13   (*Oops2*) dresolve_tac [Outpts_A_Card_form_10] 27 THEN                
    9.14 - (*Base*)  Force_tac 1
    9.15 + (*Base*)  (force_tac (local_clasimpset_of ctxt)) 1
    9.16  
    9.17  val analz_prepare_tac = 
    9.18           prepare_tac THEN
    9.19 @@ -777,7 +777,7 @@
    9.20    "to launch a few simple facts that'll help the simplifier"
    9.21  
    9.22  method_setup parts_prepare = {*
    9.23 -    Method.no_args (Method.SIMPLE_METHOD parts_prepare_tac) *}
    9.24 +    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (parts_prepare_tac ctxt)) *}
    9.25    "additional facts to reason about parts"
    9.26  
    9.27  method_setup analz_prepare = {*
    9.28 @@ -1386,10 +1386,4 @@
    9.29  apply auto
    9.30  done
    9.31  
    9.32 -
    9.33 -
    9.34 -
    9.35 -
    9.36 -
    9.37  end
    9.38 -

    10.1 --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Sat Jul 21 17:40:40 2007 +0200
    10.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Sat Jul 21 23:25:00 2007 +0200
    10.3 @@ -758,22 +758,22 @@
    10.4  val Gets_imp_knows_Spy_parts_Snd = thm "Gets_imp_knows_Spy_parts_Snd"
    10.5  val Gets_imp_knows_Spy_analz_Snd = thm "Gets_imp_knows_Spy_analz_Snd"
    10.6  
    10.7 -val prepare_tac = 
    10.8 +fun prepare_tac ctxt = 
    10.9   (*SR_U8*)   forward_tac [Outpts_B_Card_form_7] 14 THEN
   10.10 - (*SR_U8*)   Clarify_tac 15 THEN
   10.11 + (*SR_U8*)   clarify_tac (local_claset_of ctxt) 15 THEN
   10.12   (*SR_U9*)   forward_tac [Outpts_A_Card_form_4] 16 THEN 
   10.13   (*SR_U11*)  forward_tac [Outpts_A_Card_form_10] 21 
   10.14  
   10.15 -val parts_prepare_tac = 
   10.16 -           prepare_tac THEN
   10.17 +fun parts_prepare_tac ctxt = 
   10.18 +           prepare_tac ctxt THEN
   10.19   (*SR_U9*)   dresolve_tac [Gets_imp_knows_Spy_parts_Snd] 18 THEN 
   10.20   (*SR_U9*)   dresolve_tac [Gets_imp_knows_Spy_parts_Snd] 19 THEN 
   10.21   (*Oops1*) dresolve_tac [Outpts_B_Card_form_7] 25    THEN               
   10.22   (*Oops2*) dresolve_tac [Outpts_A_Card_form_10] 27 THEN                
   10.23 - (*Base*)  Force_tac 1
   10.24 + (*Base*)  (force_tac (local_clasimpset_of ctxt)) 1
   10.25  
   10.26 -val analz_prepare_tac = 
   10.27 -         prepare_tac THEN
   10.28 +fun analz_prepare_tac ctxt = 
   10.29 +         prepare_tac ctxt THEN
   10.30           dtac (Gets_imp_knows_Spy_analz_Snd) 18 THEN 
   10.31   (*SR_U9*) dtac (Gets_imp_knows_Spy_analz_Snd) 19 THEN 
   10.32           REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac)
   10.33 @@ -781,15 +781,15 @@
   10.34  *}
   10.35  
   10.36  method_setup prepare = {*
   10.37 -    Method.no_args (Method.SIMPLE_METHOD prepare_tac) *}
   10.38 +    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (prepare_tac ctxt)) *}
   10.39    "to launch a few simple facts that'll help the simplifier"
   10.40  
   10.41  method_setup parts_prepare = {*
   10.42 -    Method.no_args (Method.SIMPLE_METHOD parts_prepare_tac) *}
   10.43 +    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (parts_prepare_tac ctxt)) *}
   10.44    "additional facts to reason about parts"
   10.45  
   10.46  method_setup analz_prepare = {*
   10.47 -    Method.no_args (Method.SIMPLE_METHOD analz_prepare_tac) *}
   10.48 +    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (analz_prepare_tac ctxt)) *}
   10.49    "additional facts to reason about analz"
   10.50  
   10.51  

    11.1 --- a/src/HOL/Auth/Smartcard/Smartcard.thy	Sat Jul 21 17:40:40 2007 +0200
    11.2 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Sat Jul 21 23:25:00 2007 +0200
    11.3 @@ -359,23 +359,20 @@
    11.4  {*
    11.5  (*Omitting used_Says makes the tactic much faster: it leaves expressions
    11.6      such as  Nonce ?N \<notin> used evs that match Nonce_supply*)
    11.7 -fun gen_possibility_tac ss state = state |>
    11.8 +fun possibility_tac ctxt =
    11.9     (REPEAT 
   11.10 -    (ALLGOALS (simp_tac (ss delsimps [used_Says, used_Notes, used_Gets,
   11.11 +    (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says, used_Notes, used_Gets,
   11.12                           used_Inputs, used_C_Gets, used_Outpts, used_A_Gets] 
   11.13                           setSolver safe_solver))
   11.14       THEN
   11.15       REPEAT_FIRST (eq_assume_tac ORELSE' 
   11.16                     resolve_tac [refl, conjI, Nonce_supply])))
   11.17  
   11.18 -(*Tactic for possibility theorems (ML script version)*)
   11.19 -fun possibility_tac state = gen_possibility_tac (simpset()) state
   11.20 -
   11.21  (*For harder protocols (such as Recur) where we have to set up some
   11.22    nonces and keys initially*)
   11.23 -fun basic_possibility_tac st = st |>
   11.24 +fun basic_possibility_tac ctxt =
   11.25      REPEAT 
   11.26 -    (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
   11.27 +    (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
   11.28       THEN
   11.29       REPEAT_FIRST (resolve_tac [refl, conjI]))
   11.30  *}
   11.31 @@ -426,8 +423,8 @@
   11.32  val analz_image_freshK_lemma = thm "analz_image_freshK_lemma";
   11.33  
   11.34  val analz_image_freshK_ss = 
   11.35 -     simpset() delsimps [image_insert, image_Un]
   11.36 -	       delsimps [imp_disjL]    (*reduces blow-up*)
   11.37 +     @{simpset} delsimps [image_insert, image_Un]
   11.38 +	       delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
   11.39  	       addsimps thms "analz_image_freshK_simps"
   11.40  *}
   11.41  
   11.42 @@ -450,11 +447,16 @@
   11.43  
   11.44  method_setup possibility = {*
   11.45      Method.ctxt_args (fn ctxt =>
   11.46 -        Method.SIMPLE_METHOD (gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
   11.47 +        Method.SIMPLE_METHOD (possibility_tac ctxt)) *}
   11.48 +    "for proving possibility theorems"
   11.49 +
   11.50 +method_setup basic_possibility = {*
   11.51 +    Method.ctxt_args (fn ctxt =>
   11.52 +        Method.SIMPLE_METHOD (basic_possibility_tac ctxt)) *}
   11.53      "for proving possibility theorems"
   11.54  
   11.55  lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
   11.56 -by (induct e, auto simp: knows_Cons)
   11.57 +by (induct e) (auto simp: knows_Cons)
   11.58  
   11.59  (*Needed for actual protocols that will follow*)
   11.60  declare shrK_disj_crdK[THEN not_sym, iff]
   11.61 @@ -466,8 +468,4 @@
   11.62  
   11.63  declare legalUse_def [iff] illegalUse_def [iff]
   11.64  
   11.65 -
   11.66 -
   11.67 -
   11.68 -
   11.69  end

    12.1 --- a/src/HOL/Bali/AxCompl.thy	Sat Jul 21 17:40:40 2007 +0200
    12.2 +++ b/src/HOL/Bali/AxCompl.thy	Sat Jul 21 23:25:00 2007 +0200
    12.3 @@ -1404,7 +1404,7 @@
    12.4  using finU uA
    12.5  apply -
    12.6  apply (induct_tac "n")
    12.7 -apply  (tactic "ALLGOALS Clarsimp_tac")
    12.8 +apply  (tactic "ALLGOALS (clarsimp_tac @{clasimpset})")
    12.9  apply  (tactic {* dtac (permute_prems 0 1 (thm "card_seteq")) 1 *})
   12.10  apply    simp
   12.11  apply   (erule finite_imageI)

    13.1 --- a/src/HOL/Bali/AxSem.thy	Sat Jul 21 17:40:40 2007 +0200
    13.2 +++ b/src/HOL/Bali/AxSem.thy	Sat Jul 21 23:25:00 2007 +0200
    13.3 @@ -670,7 +670,7 @@
    13.4  lemma ax_thin [rule_format (no_asm)]: 
    13.5    "G,(A'::'a triple set)|\<turnstile>(ts::'a triple set) \<Longrightarrow> \<forall>A. A' \<subseteq> A \<longrightarrow> G,A|\<turnstile>ts"
    13.6  apply (erule ax_derivs.induct)
    13.7 -apply                (tactic "ALLGOALS(EVERY'[Clarify_tac,REPEAT o smp_tac 1])")
    13.8 +apply                (tactic "ALLGOALS(EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1])")
    13.9  apply                (rule ax_derivs.empty)
   13.10  apply               (erule (1) ax_derivs.insert)
   13.11  apply              (fast intro: ax_derivs.asm)
   13.12 @@ -712,7 +712,7 @@
   13.13  apply  (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))
   13.14  (*37 subgoals*)
   13.15  apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
   13.16 -                   THEN_ALL_NEW Fast_tac) *})
   13.17 +                   THEN_ALL_NEW fast_tac @{claset}) *})
   13.18  (*1 subgoal*)
   13.19  apply (clarsimp simp add: subset_mtriples_iff)
   13.20  apply (rule ax_derivs.Methd)

    14.1 --- a/src/HOL/HoareParallel/Gar_Coll.thy	Sat Jul 21 17:40:40 2007 +0200
    14.2 +++ b/src/HOL/HoareParallel/Gar_Coll.thy	Sat Jul 21 23:25:00 2007 +0200
    14.3 @@ -792,7 +792,7 @@
    14.4  --{* 32 subgoals left *}
    14.5  apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
    14.6  --{* 20 subgoals left *}
    14.7 -apply(tactic{* TRYALL Clarify_tac *})
    14.8 +apply(tactic{* TRYALL (clarify_tac @{claset}) *})
    14.9  apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
   14.10  apply(tactic {* TRYALL (etac disjE) *})
   14.11  apply simp_all
   14.12 @@ -812,7 +812,7 @@
   14.13  apply(tactic  {* TRYALL (interfree_aux_tac) *})
   14.14  --{* 64 subgoals left *}
   14.15  apply(simp_all add:nth_list_update Invariants Append_to_free0)+
   14.16 -apply(tactic{* TRYALL Clarify_tac *})
   14.17 +apply(tactic{* TRYALL (clarify_tac @{claset}) *})
   14.18  --{* 4 subgoals left *}
   14.19  apply force
   14.20  apply(simp add:Append_to_free2)

    15.1 --- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Sat Jul 21 17:40:40 2007 +0200
    15.2 +++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Sat Jul 21 23:25:00 2007 +0200
    15.3 @@ -133,7 +133,7 @@
    15.4  apply(simp_all add:mul_mutator_interfree)
    15.5  apply(simp_all add: mul_mutator_defs)
    15.6  apply(tactic {* TRYALL (interfree_aux_tac) *})
    15.7 -apply(tactic {* ALLGOALS Clarify_tac *})
    15.8 +apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
    15.9  apply (simp_all add:nth_list_update)
   15.10  done
   15.11  
   15.12 @@ -1135,7 +1135,7 @@
   15.13    interfree_aux (Some(Mul_Append n),{}, Some(Mul_Redirect_Edge j n))"
   15.14  apply (unfold mul_modules)
   15.15  apply interfree_aux
   15.16 -apply(tactic {* ALLGOALS Clarify_tac *})
   15.17 +apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
   15.18  apply(simp_all add:Graph6 Append_to_free0 Append_to_free1 mul_collector_defs mul_mutator_defs Mul_AppendInv_def)
   15.19  apply(erule_tac x=j in allE, force dest:Graph3)+
   15.20  done
   15.21 @@ -1144,7 +1144,7 @@
   15.22    interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Append n))"
   15.23  apply (unfold mul_modules)
   15.24  apply interfree_aux
   15.25 -apply(tactic {* ALLGOALS Clarify_tac *})
   15.26 +apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
   15.27  apply(simp_all add:mul_collector_defs Append_to_free0 Mul_AppendInv_def  mul_mutator_defs nth_list_update)
   15.28  done
   15.29  
   15.30 @@ -1152,7 +1152,7 @@
   15.31    interfree_aux (Some(Mul_Append n),{}, Some(Mul_Color_Target j n))"
   15.32  apply (unfold mul_modules)
   15.33  apply interfree_aux
   15.34 -apply(tactic {* ALLGOALS Clarify_tac *})
   15.35 +apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
   15.36  apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_AppendInv_def Graph7 Graph8 Append_to_free0 Append_to_free1 
   15.37                Graph12 nth_list_update)
   15.38  done
   15.39 @@ -1161,7 +1161,7 @@
   15.40    interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Append n))"
   15.41  apply (unfold mul_modules)
   15.42  apply interfree_aux
   15.43 -apply(tactic {* ALLGOALS Clarify_tac *})
   15.44 +apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
   15.45  apply(simp_all add: mul_mutator_defs nth_list_update)
   15.46  apply(simp add:Mul_AppendInv_def Append_to_free0)
   15.47  done
   15.48 @@ -1190,7 +1190,7 @@
   15.49  --{* 24 subgoals left *}
   15.50  apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
   15.51  --{* 14 subgoals left *}
   15.52 -apply(tactic {* TRYALL Clarify_tac *})
   15.53 +apply(tactic {* TRYALL (clarify_tac @{claset}) *})
   15.54  apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
   15.55  apply(tactic {* TRYALL (rtac conjI) *})
   15.56  apply(tactic {* TRYALL (rtac impI) *})

    16.1 --- a/src/HOL/HoareParallel/OG_Examples.thy	Sat Jul 21 17:40:40 2007 +0200
    16.2 +++ b/src/HOL/HoareParallel/OG_Examples.thy	Sat Jul 21 23:25:00 2007 +0200
    16.3 @@ -171,10 +171,10 @@
    16.4  --{* 35 vc *}
    16.5  apply simp_all
    16.6  --{* 21 vc *}
    16.7 -apply(tactic {* ALLGOALS Clarify_tac *})
    16.8 +apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
    16.9  --{* 11 vc *}
   16.10  apply simp_all
   16.11 -apply(tactic {* ALLGOALS Clarify_tac *})
   16.12 +apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
   16.13  --{* 10 subgoals left *}
   16.14  apply(erule less_SucE)
   16.15   apply simp
   16.16 @@ -431,17 +431,17 @@
   16.17   .{ \<forall>k<length a. (a ! k)=(\<acute>b ! k)}."
   16.18  apply oghoare
   16.19  --{* 138 vc  *}
   16.20 -apply(tactic {* ALLGOALS Clarify_tac *})
   16.21 +apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
   16.22  --{* 112 subgoals left *}
   16.23  apply(simp_all (no_asm))
   16.24  apply(tactic {*ALLGOALS (conjI_Tac (K all_tac)) *})
   16.25  --{* 930 subgoals left *}
   16.26 -apply(tactic {* ALLGOALS Clarify_tac *})
   16.27 +apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
   16.28  apply(simp_all (asm_lr) only:length_0_conv [THEN sym])
   16.29  --{* 44 subgoals left *}
   16.30  apply (simp_all (asm_lr) del:length_0_conv add: nth_list_update mod_less_divisor mod_lemma)
   16.31  --{* 32 subgoals left *}
   16.32 -apply(tactic {* ALLGOALS Clarify_tac *})
   16.33 +apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
   16.34  
   16.35  apply(tactic {* TRYALL simple_arith_tac *})
   16.36  --{* 9 subgoals left *}
   16.37 @@ -538,7 +538,7 @@
   16.38   .{\<acute>x=n}."
   16.39  apply oghoare
   16.40  apply (simp_all cong del: strong_setsum_cong)
   16.41 -apply (tactic {* ALLGOALS Clarify_tac *})
   16.42 +apply (tactic {* ALLGOALS (clarify_tac @{claset}) *})
   16.43  apply (simp_all cong del: strong_setsum_cong)
   16.44     apply(erule (1) Example2_lemma2)
   16.45    apply(erule (1) Example2_lemma2)

    17.1 --- a/src/HOL/HoareParallel/OG_Tactics.thy	Sat Jul 21 17:40:40 2007 +0200
    17.2 +++ b/src/HOL/HoareParallel/OG_Tactics.thy	Sat Jul 21 23:25:00 2007 +0200
    17.3 @@ -320,119 +320,119 @@
    17.4  
    17.5  ML {*
    17.6  
    17.7 - fun WlpTac i = (rtac (thm "SeqRule") i) THEN (HoareRuleTac false (i+1))
    17.8 + fun WlpTac i = (rtac (@{thm SeqRule}) i) THEN (HoareRuleTac false (i+1))
    17.9  and HoareRuleTac precond i st = st |>  
   17.10      ( (WlpTac i THEN HoareRuleTac precond i)
   17.11        ORELSE
   17.12 -      (FIRST[rtac (thm "SkipRule") i,
   17.13 -             rtac (thm "BasicRule") i,
   17.14 -             EVERY[rtac (thm "ParallelConseqRule") i,
   17.15 +      (FIRST[rtac (@{thm SkipRule}) i,
   17.16 +             rtac (@{thm BasicRule}) i,
   17.17 +             EVERY[rtac (@{thm ParallelConseqRule}) i,
   17.18                     ParallelConseq (i+2),
   17.19                     ParallelTac (i+1),
   17.20                     ParallelConseq i], 
   17.21 -             EVERY[rtac (thm "CondRule") i,
   17.22 +             EVERY[rtac (@{thm CondRule}) i,
   17.23                     HoareRuleTac false (i+2),
   17.24                     HoareRuleTac false (i+1)],
   17.25 -             EVERY[rtac (thm "WhileRule") i,
   17.26 +             EVERY[rtac (@{thm WhileRule}) i,
   17.27                     HoareRuleTac true (i+1)],
   17.28               K all_tac i ]
   17.29 -       THEN (if precond then (K all_tac i) else (rtac (thm "subset_refl") i))))
   17.30 +       THEN (if precond then (K all_tac i) else (rtac (@{thm subset_refl}) i))))
   17.31  
   17.32 -and  AnnWlpTac i = (rtac (thm "AnnSeq") i) THEN (AnnHoareRuleTac (i+1))
   17.33 +and  AnnWlpTac i = (rtac (@{thm AnnSeq}) i) THEN (AnnHoareRuleTac (i+1))
   17.34  and AnnHoareRuleTac i st = st |>  
   17.35      ( (AnnWlpTac i THEN AnnHoareRuleTac i )
   17.36       ORELSE
   17.37 -      (FIRST[(rtac (thm "AnnskipRule") i),
   17.38 -             EVERY[rtac (thm "AnnatomRule") i,
   17.39 +      (FIRST[(rtac (@{thm AnnskipRule}) i),
   17.40 +             EVERY[rtac (@{thm AnnatomRule}) i,
   17.41                     HoareRuleTac true (i+1)],
   17.42 -             (rtac (thm "AnnwaitRule") i),
   17.43 -             rtac (thm "AnnBasic") i,
   17.44 -             EVERY[rtac (thm "AnnCond1") i,
   17.45 +             (rtac (@{thm AnnwaitRule}) i),
   17.46 +             rtac (@{thm AnnBasic}) i,
   17.47 +             EVERY[rtac (@{thm AnnCond1}) i,
   17.48                     AnnHoareRuleTac (i+3),
   17.49                     AnnHoareRuleTac (i+1)],
   17.50 -             EVERY[rtac (thm "AnnCond2") i,
   17.51 +             EVERY[rtac (@{thm AnnCond2}) i,
   17.52                     AnnHoareRuleTac (i+1)],
   17.53 -             EVERY[rtac (thm "AnnWhile") i,
   17.54 +             EVERY[rtac (@{thm AnnWhile}) i,
   17.55                     AnnHoareRuleTac (i+2)],
   17.56 -             EVERY[rtac (thm "AnnAwait") i,
   17.57 +             EVERY[rtac (@{thm AnnAwait}) i,
   17.58                     HoareRuleTac true (i+1)],
   17.59               K all_tac i]))
   17.60  
   17.61 -and ParallelTac i = EVERY[rtac (thm "ParallelRule") i,
   17.62 +and ParallelTac i = EVERY[rtac (@{thm ParallelRule}) i,
   17.63                            interfree_Tac (i+1),
   17.64                             MapAnn_Tac i]
   17.65  
   17.66  and MapAnn_Tac i st = st |>
   17.67 -    (FIRST[rtac (thm "MapAnnEmpty") i,
   17.68 -           EVERY[rtac (thm "MapAnnList") i,
   17.69 +    (FIRST[rtac (@{thm MapAnnEmpty}) i,
   17.70 +           EVERY[rtac (@{thm MapAnnList}) i,
   17.71                   MapAnn_Tac (i+1),
   17.72                   AnnHoareRuleTac i],
   17.73 -           EVERY[rtac (thm "MapAnnMap") i,
   17.74 -                 rtac (thm "allI") i,rtac (thm "impI") i,
   17.75 +           EVERY[rtac (@{thm MapAnnMap}) i,
   17.76 +                 rtac (@{thm allI}) i,rtac (@{thm impI}) i,
   17.77                   AnnHoareRuleTac i]])
   17.78  
   17.79  and interfree_swap_Tac i st = st |>
   17.80 -    (FIRST[rtac (thm "interfree_swap_Empty") i,
   17.81 -           EVERY[rtac (thm "interfree_swap_List") i,
   17.82 +    (FIRST[rtac (@{thm interfree_swap_Empty}) i,
   17.83 +           EVERY[rtac (@{thm interfree_swap_List}) i,
   17.84                   interfree_swap_Tac (i+2),
   17.85                   interfree_aux_Tac (i+1),
   17.86                   interfree_aux_Tac i ],
   17.87 -           EVERY[rtac (thm "interfree_swap_Map") i,
   17.88 -                 rtac (thm "allI") i,rtac (thm "impI") i,
   17.89 +           EVERY[rtac (@{thm interfree_swap_Map}) i,
   17.90 +                 rtac (@{thm allI}) i,rtac (@{thm impI}) i,
   17.91                   conjI_Tac (interfree_aux_Tac) i]])
   17.92  
   17.93  and interfree_Tac i st = st |> 
   17.94 -   (FIRST[rtac (thm "interfree_Empty") i,
   17.95 -          EVERY[rtac (thm "interfree_List") i,
   17.96 +   (FIRST[rtac (@{thm interfree_Empty}) i,
   17.97 +          EVERY[rtac (@{thm interfree_List}) i,
   17.98                  interfree_Tac (i+1),
   17.99                  interfree_swap_Tac i],
  17.100 -          EVERY[rtac (thm "interfree_Map") i,
  17.101 -                rtac (thm "allI") i,rtac (thm "allI") i,rtac (thm "impI") i,
  17.102 +          EVERY[rtac (@{thm interfree_Map}) i,
  17.103 +                rtac (@{thm allI}) i,rtac (@{thm allI}) i,rtac (@{thm impI}) i,
  17.104                  interfree_aux_Tac i ]])
  17.105  
  17.106  and interfree_aux_Tac i = (before_interfree_simp_tac i ) THEN 
  17.107 -        (FIRST[rtac (thm "interfree_aux_rule1") i,
  17.108 +        (FIRST[rtac (@{thm interfree_aux_rule1}) i,
  17.109                 dest_assertions_Tac i])
  17.110  
  17.111  and dest_assertions_Tac i st = st |>
  17.112 -    (FIRST[EVERY[rtac (thm "AnnBasic_assertions") i,
  17.113 +    (FIRST[EVERY[rtac (@{thm AnnBasic_assertions}) i,
  17.114                   dest_atomics_Tac (i+1),
  17.115                   dest_atomics_Tac i],
  17.116 -           EVERY[rtac (thm "AnnSeq_assertions") i,
  17.117 +           EVERY[rtac (@{thm AnnSeq_assertions}) i,
  17.118                   dest_assertions_Tac (i+1),
  17.119                   dest_assertions_Tac i],
  17.120 -           EVERY[rtac (thm "AnnCond1_assertions") i,
  17.121 +           EVERY[rtac (@{thm AnnCond1_assertions}) i,
  17.122                   dest_assertions_Tac (i+2),
  17.123                   dest_assertions_Tac (i+1),
  17.124                   dest_atomics_Tac i],
  17.125 -           EVERY[rtac (thm "AnnCond2_assertions") i,
  17.126 +           EVERY[rtac (@{thm AnnCond2_assertions}) i,
  17.127                   dest_assertions_Tac (i+1),
  17.128                   dest_atomics_Tac i],
  17.129 -           EVERY[rtac (thm "AnnWhile_assertions") i,
  17.130 +           EVERY[rtac (@{thm AnnWhile_assertions}) i,
  17.131                   dest_assertions_Tac (i+2),
  17.132                   dest_atomics_Tac (i+1),
  17.133                   dest_atomics_Tac i],
  17.134 -           EVERY[rtac (thm "AnnAwait_assertions") i,
  17.135 +           EVERY[rtac (@{thm AnnAwait_assertions}) i,
  17.136                   dest_atomics_Tac (i+1),
  17.137                   dest_atomics_Tac i],
  17.138             dest_atomics_Tac i])
  17.139  
  17.140  and dest_atomics_Tac i st = st |>
  17.141 -    (FIRST[EVERY[rtac (thm "AnnBasic_atomics") i,
  17.142 +    (FIRST[EVERY[rtac (@{thm AnnBasic_atomics}) i,
  17.143                   HoareRuleTac true i],
  17.144 -           EVERY[rtac (thm "AnnSeq_atomics") i,
  17.145 +           EVERY[rtac (@{thm AnnSeq_atomics}) i,
  17.146                   dest_atomics_Tac (i+1),
  17.147                   dest_atomics_Tac i],
  17.148 -           EVERY[rtac (thm "AnnCond1_atomics") i,
  17.149 +           EVERY[rtac (@{thm AnnCond1_atomics}) i,
  17.150                   dest_atomics_Tac (i+1),
  17.151                   dest_atomics_Tac i],
  17.152 -           EVERY[rtac (thm "AnnCond2_atomics") i,
  17.153 +           EVERY[rtac (@{thm AnnCond2_atomics}) i,
  17.154                   dest_atomics_Tac i],
  17.155 -           EVERY[rtac (thm "AnnWhile_atomics") i,
  17.156 +           EVERY[rtac (@{thm AnnWhile_atomics}) i,
  17.157                   dest_atomics_Tac i],
  17.158 -           EVERY[rtac (thm "Annatom_atomics") i,
  17.159 +           EVERY[rtac (@{thm Annatom_atomics}) i,
  17.160                   HoareRuleTac true i],
  17.161 -           EVERY[rtac (thm "AnnAwait_atomics") i,
  17.162 +           EVERY[rtac (@{thm AnnAwait_atomics}) i,
  17.163                   HoareRuleTac true i],
  17.164                   K all_tac i])
  17.165  *}
  17.166 @@ -441,8 +441,8 @@
  17.167  text {* The final tactic is given the name @{text oghoare}: *}
  17.168  
  17.169  ML {* 
  17.170 -fun oghoare_tac i thm = SUBGOAL (fn (term, _) =>
  17.171 -   (HoareRuleTac true i)) i thm
  17.172 +val oghoare_tac = SUBGOAL (fn (_, i) =>
  17.173 +   (HoareRuleTac true i))
  17.174  *}
  17.175  
  17.176  text {* Notice that the tactic for parallel programs @{text
  17.177 @@ -453,11 +453,11 @@
  17.178  verification conditions for annotated sequential programs and to
  17.179  generate verification conditions out of interference freedom tests: *}
  17.180  
  17.181 -ML {* fun annhoare_tac i thm = SUBGOAL (fn (term, _) =>
  17.182 -  (AnnHoareRuleTac i)) i thm
  17.183 +ML {* val annhoare_tac = SUBGOAL (fn (_, i) =>
  17.184 +  (AnnHoareRuleTac i))
  17.185  
  17.186 -fun interfree_aux_tac i thm = SUBGOAL (fn (term, _) =>
  17.187 -   (interfree_aux_Tac i)) i thm
  17.188 +val interfree_aux_tac = SUBGOAL (fn (_, i) =>
  17.189 +   (interfree_aux_Tac i))
  17.190  *}
  17.191  
  17.192  text {* The so defined ML tactics are then ``exported'' to be used in

    18.1 --- a/src/HOL/IMPP/Hoare.thy	Sat Jul 21 17:40:40 2007 +0200
    18.2 +++ b/src/HOL/IMPP/Hoare.thy	Sat Jul 21 23:25:00 2007 +0200
    18.3 @@ -206,7 +206,7 @@
    18.4  *)
    18.5  lemma thin [rule_format]: "G'||-ts ==> !G. G' <= G --> G||-ts"
    18.6  apply (erule hoare_derivs.induct)
    18.7 -apply                (tactic {* ALLGOALS (EVERY'[Clarify_tac, REPEAT o smp_tac 1]) *})
    18.8 +apply                (tactic {* ALLGOALS (EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
    18.9  apply (rule hoare_derivs.empty)
   18.10  apply               (erule (1) hoare_derivs.insert)
   18.11  apply              (fast intro: hoare_derivs.asm)

    19.1 --- a/src/HOL/MicroJava/J/Example.thy	Sat Jul 21 17:40:40 2007 +0200
    19.2 +++ b/src/HOL/MicroJava/J/Example.thy	Sat Jul 21 23:25:00 2007 +0200
    19.3 @@ -373,7 +373,7 @@
    19.4  apply (auto simp add: appl_methds_foo_Base)
    19.5  done
    19.6  
    19.7 -ML {* fun t thm = resolve_tac (thms "ty_expr_ty_exprs_wt_stmt.intros") 1 thm *}
    19.8 +ML {* val t = resolve_tac @{thms ty_expr_ty_exprs_wt_stmt.intros} 1 *}
    19.9  lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>  
   19.10    Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>"
   19.11  apply (tactic t) -- ";;"
   19.12 @@ -399,7 +399,7 @@
   19.13  apply (rule max_spec_foo_Base)
   19.14  done
   19.15  
   19.16 -ML {* fun e t = resolve_tac (thm "NewCI"::thms "eval_evals_exec.intros") 1 t *}
   19.17 +ML {* val e = resolve_tac (@{thm NewCI} :: @{thms eval_evals_exec.intros}) 1 *}
   19.18  
   19.19  declare split_if [split del]
   19.20  declare init_vars_def [simp] c_hupd_def [simp] cast_ok_def [simp]

    20.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Sat Jul 21 17:40:40 2007 +0200
    20.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Sat Jul 21 23:25:00 2007 +0200
    20.3 @@ -206,7 +206,7 @@
    20.4  apply( simp_all)
    20.5  apply( tactic "ALLGOALS strip_tac")
    20.6  apply( tactic {* ALLGOALS (eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"]
    20.7 -                 THEN_ALL_NEW Full_simp_tac) *})
    20.8 +                 THEN_ALL_NEW (full_simp_tac (simpset_of @{theory Conform}))) *})
    20.9  apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
   20.10  
   20.11  -- "Level 7"
   20.12 @@ -246,10 +246,11 @@
   20.13  
   20.14  -- "for FAss"
   20.15  apply( tactic {* EVERY'[eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"] 
   20.16 -       THEN_ALL_NEW Full_simp_tac, REPEAT o (etac conjE), hyp_subst_tac] 3*})
   20.17 +       THEN_ALL_NEW (full_simp_tac @{simpset}), REPEAT o (etac conjE), hyp_subst_tac] 3*})
   20.18  
   20.19  -- "for if"
   20.20 -apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 7*})
   20.21 +apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW
   20.22 +  (asm_full_simp_tac @{simpset})) 7*})
   20.23  
   20.24  apply (tactic "forward_hyp_tac")
   20.25  
   20.26 @@ -281,7 +282,7 @@
   20.27  -- "7 LAss"
   20.28  apply (fold fun_upd_def)
   20.29  apply( tactic {* (eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"] 
   20.30 -                 THEN_ALL_NEW Full_simp_tac) 1 *})
   20.31 +                 THEN_ALL_NEW (full_simp_tac @{simpset})) 1 *})
   20.32  apply (intro strip)
   20.33  apply (case_tac E)
   20.34  apply (simp)

    21.1 --- a/src/HOL/NanoJava/AxSem.thy	Sat Jul 21 17:40:40 2007 +0200
    21.2 +++ b/src/HOL/NanoJava/AxSem.thy	Sat Jul 21 23:25:00 2007 +0200
    21.3 @@ -153,7 +153,7 @@
    21.4    "(A' |\<turnstile>  C         \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A |\<turnstile>  C       )) \<and> 
    21.5     (A'  \<turnstile>\<^sub>e {P} e {Q} \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A  \<turnstile>\<^sub>e {P} e {Q}))"
    21.6  apply (rule hoare_ehoare.induct)
    21.7 -apply (tactic "ALLGOALS(EVERY'[Clarify_tac, REPEAT o smp_tac 1])")
    21.8 +apply (tactic "ALLGOALS(EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1])")
    21.9  apply (blast intro: hoare_ehoare.Skip)
   21.10  apply (blast intro: hoare_ehoare.Comp)
   21.11  apply (blast intro: hoare_ehoare.Cond)

    22.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Jul 21 17:40:40 2007 +0200
    22.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Jul 21 23:25:00 2007 +0200
    22.3 @@ -18,8 +18,8 @@
    22.4  structure NominalAtoms : NOMINAL_ATOMS =
    22.5  struct
    22.6  
    22.7 -val finite_emptyI = thm "finite.emptyI";
    22.8 -val Collect_const = thm "Collect_const";
    22.9 +val finite_emptyI = @{thm "finite.emptyI"};
   22.10 +val Collect_const = @{thm "Collect_const"};
   22.11  
   22.12  
   22.13  (* theory data *)
   22.14 @@ -60,6 +60,8 @@
   22.15  (* atom_decl <ak1> ... <akn>                           *)
   22.16  fun create_nom_typedecls ak_names thy =
   22.17    let
   22.18 +    val cla_s = claset_of thy;
   22.19 +
   22.20      (* declares a type-decl for every atom-kind: *) 
   22.21      (* that is typedecl <ak>                     *)
   22.22      val thy1 = TypedefPackage.add_typedecls (map (fn x => (x,[],NoSyn)) ak_names) thy;
   22.23 @@ -184,7 +186,7 @@
   22.24  	val name = "at_"^ak_name^ "_inst";
   22.25          val statement = HOLogic.mk_Trueprop (cat $ at_type);
   22.26  
   22.27 -        val proof = fn _ => auto_tac (claset(),simp_s);
   22.28 +        val proof = fn _ => auto_tac (cla_s,simp_s);
   22.29  
   22.30        in 
   22.31          ((name, Goal.prove_global thy5 [] [] statement proof), []) 
   22.32 @@ -246,7 +248,7 @@
   22.33  	val name = "pt_"^ak_name^ "_inst";
   22.34          val statement = HOLogic.mk_Trueprop (cpt $ pt_type $ at_type);
   22.35  
   22.36 -        val proof = fn _ => auto_tac (claset(),simp_s);
   22.37 +        val proof = fn _ => auto_tac (cla_s,simp_s);
   22.38        in 
   22.39          ((name, Goal.prove_global thy7 [] [] statement proof), []) 
   22.40        end) ak_names_types);
   22.41 @@ -291,7 +293,7 @@
   22.42  	 val name = "fs_"^ak_name^ "_inst";
   22.43           val statement = HOLogic.mk_Trueprop (cfs $ fs_type $ at_type);
   22.44  
   22.45 -         val proof = fn _ => auto_tac (claset(),simp_s);
   22.46 +         val proof = fn _ => auto_tac (cla_s,simp_s);
   22.47         in 
   22.48           ((name, Goal.prove_global thy11 [] [] statement proof), []) 
   22.49         end) ak_names_types);
   22.50 @@ -342,7 +344,7 @@
   22.51  	     val name = "cp_"^ak_name^ "_"^ak_name'^"_inst";
   22.52               val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type');
   22.53  
   22.54 -             val proof = fn _ => EVERY [auto_tac (claset(),simp_s), rtac cp1 1];
   22.55 +             val proof = fn _ => EVERY [auto_tac (cla_s,simp_s), rtac cp1 1];
   22.56  	   in
   22.57  	     PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy'
   22.58  	   end) 
   22.59 @@ -373,7 +375,7 @@
   22.60  	         val name = "dj_"^ak_name^"_"^ak_name';
   22.61                   val statement = HOLogic.mk_Trueprop (cdj $ at_type $ at_type');
   22.62  
   22.63 -                 val proof = fn _ => auto_tac (claset(),simp_s);
   22.64 +                 val proof = fn _ => auto_tac (cla_s,simp_s);
   22.65  	       in
   22.66  		PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy'
   22.67  	       end
   22.68 @@ -384,18 +386,18 @@
   22.69       (********  pt_<ak> class instances  ********)
   22.70       (*=========================================*)
   22.71       (* some abbreviations for theorems *)
   22.72 -      val pt1           = thm "pt1";
   22.73 -      val pt2           = thm "pt2";
   22.74 -      val pt3           = thm "pt3";
   22.75 -      val at_pt_inst    = thm "at_pt_inst";
   22.76 -      val pt_set_inst   = thm "pt_set_inst"; 
   22.77 -      val pt_unit_inst  = thm "pt_unit_inst";
   22.78 -      val pt_prod_inst  = thm "pt_prod_inst"; 
   22.79 -      val pt_nprod_inst = thm "pt_nprod_inst"; 
   22.80 -      val pt_list_inst  = thm "pt_list_inst";   
   22.81 -      val pt_optn_inst  = thm "pt_option_inst";   
   22.82 -      val pt_noptn_inst = thm "pt_noption_inst";   
   22.83 -      val pt_fun_inst   = thm "pt_fun_inst";     
   22.84 +      val pt1           = @{thm "pt1"};
   22.85 +      val pt2           = @{thm "pt2"};
   22.86 +      val pt3           = @{thm "pt3"};
   22.87 +      val at_pt_inst    = @{thm "at_pt_inst"};
   22.88 +      val pt_set_inst   = @{thm "pt_set_inst"}; 
   22.89 +      val pt_unit_inst  = @{thm "pt_unit_inst"};
   22.90 +      val pt_prod_inst  = @{thm "pt_prod_inst"}; 
   22.91 +      val pt_nprod_inst = @{thm "pt_nprod_inst"}; 
   22.92 +      val pt_list_inst  = @{thm "pt_list_inst"};
   22.93 +      val pt_optn_inst  = @{thm "pt_option_inst"};
   22.94 +      val pt_noptn_inst = @{thm "pt_noption_inst"};
   22.95 +      val pt_fun_inst   = @{thm "pt_fun_inst"};
   22.96  
   22.97       (* for all atom-kind combinations <ak>/<ak'> show that        *)
   22.98       (* every <ak> is an instance of pt_<ak'>; the proof for       *)
   22.99 @@ -466,14 +468,14 @@
  22.100         (********  fs_<ak> class instances  ********)
  22.101         (*=========================================*)
  22.102         (* abbreviations for some lemmas *)
  22.103 -       val fs1            = thm "fs1";
  22.104 -       val fs_at_inst     = thm "fs_at_inst";
  22.105 -       val fs_unit_inst   = thm "fs_unit_inst";
  22.106 -       val fs_prod_inst   = thm "fs_prod_inst";
  22.107 -       val fs_nprod_inst  = thm "fs_nprod_inst";
  22.108 -       val fs_list_inst   = thm "fs_list_inst";
  22.109 -       val fs_option_inst = thm "fs_option_inst";
  22.110 -       val dj_supp        = thm "dj_supp"
  22.111 +       val fs1            = @{thm "fs1"};
  22.112 +       val fs_at_inst     = @{thm "fs_at_inst"};
  22.113 +       val fs_unit_inst   = @{thm "fs_unit_inst"};
  22.114 +       val fs_prod_inst   = @{thm "fs_prod_inst"};
  22.115 +       val fs_nprod_inst  = @{thm "fs_nprod_inst"};
  22.116 +       val fs_list_inst   = @{thm "fs_list_inst"};
  22.117 +       val fs_option_inst = @{thm "fs_option_inst"};
  22.118 +       val dj_supp        = @{thm "dj_supp"};
  22.119  
  22.120         (* shows that <ak> is an instance of fs_<ak>     *)
  22.121         (* uses the theorem at_<ak>_inst                 *)
  22.122 @@ -528,18 +530,18 @@
  22.123         (********  cp_<ak>_<ai> class instances  ********)
  22.124         (*==============================================*)
  22.125         (* abbreviations for some lemmas *)
  22.126 -       val cp1             = thm "cp1";
  22.127 -       val cp_unit_inst    = thm "cp_unit_inst";
  22.128 -       val cp_bool_inst    = thm "cp_bool_inst";
  22.129 -       val cp_prod_inst    = thm "cp_prod_inst";
  22.130 -       val cp_list_inst    = thm "cp_list_inst";
  22.131 -       val cp_fun_inst     = thm "cp_fun_inst";
  22.132 -       val cp_option_inst  = thm "cp_option_inst";
  22.133 -       val cp_noption_inst = thm "cp_noption_inst";
  22.134 -       val cp_set_inst     = thm "cp_set_inst";
  22.135 -       val pt_perm_compose = thm "pt_perm_compose";
  22.136 +       val cp1             = @{thm "cp1"};
  22.137 +       val cp_unit_inst    = @{thm "cp_unit_inst"};
  22.138 +       val cp_bool_inst    = @{thm "cp_bool_inst"};
  22.139 +       val cp_prod_inst    = @{thm "cp_prod_inst"};
  22.140 +       val cp_list_inst    = @{thm "cp_list_inst"};
  22.141 +       val cp_fun_inst     = @{thm "cp_fun_inst"};
  22.142 +       val cp_option_inst  = @{thm "cp_option_inst"};
  22.143 +       val cp_noption_inst = @{thm "cp_noption_inst"};
  22.144 +       val cp_set_inst     = @{thm "cp_set_inst"};
  22.145 +       val pt_perm_compose = @{thm "pt_perm_compose"};
  22.146  
  22.147 -       val dj_pp_forget    = thm "dj_perm_perm_forget";
  22.148 +       val dj_pp_forget    = @{thm "dj_perm_perm_forget"};
  22.149  
  22.150         (* shows that <aj> is an instance of cp_<ak>_<ai>  *)
  22.151         (* for every  <ak>/<ai>-combination                *)
  22.152 @@ -630,7 +632,7 @@
  22.153  	     fold (fn ak_name => fn thy =>
  22.154  	     let
  22.155  	       val qu_class = Sign.full_name thy ("fs_"^ak_name);
  22.156 -	       val supp_def = thm "Nominal.supp_def";
  22.157 +	       val supp_def = @{thm "Nominal.supp_def"};
  22.158                 val simp_s = HOL_ss addsimps [supp_def,Collect_const,finite_emptyI,defn];
  22.159                 val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
  22.160               in 
  22.161 @@ -641,7 +643,7 @@
  22.162  	     fold (fn ak_name' => (fold (fn ak_name => fn thy =>
  22.163  	     let
  22.164  	       val qu_class = Sign.full_name thy ("cp_"^ak_name^"_"^ak_name');
  22.165 -	       val supp_def = thm "Nominal.supp_def";
  22.166 +	       val supp_def = @{thm "Nominal.supp_def"};
  22.167                 val simp_s = HOL_ss addsimps [defn];
  22.168                 val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
  22.169               in
  22.170 @@ -650,70 +652,70 @@
  22.171  
  22.172          in
  22.173           thy26
  22.174 -         |> discrete_pt_inst "nat"  (thm "perm_nat_def")
  22.175 -         |> discrete_fs_inst "nat"  (thm "perm_nat_def") 
  22.176 -         |> discrete_cp_inst "nat"  (thm "perm_nat_def") 
  22.177 -         |> discrete_pt_inst "bool" (thm "perm_bool")
  22.178 -         |> discrete_fs_inst "bool" (thm "perm_bool")
  22.179 -         |> discrete_cp_inst "bool" (thm "perm_bool")
  22.180 -         |> discrete_pt_inst "IntDef.int" (thm "perm_int_def")
  22.181 -         |> discrete_fs_inst "IntDef.int" (thm "perm_int_def") 
  22.182 -         |> discrete_cp_inst "IntDef.int" (thm "perm_int_def") 
  22.183 -         |> discrete_pt_inst "List.char" (thm "perm_char_def")
  22.184 -         |> discrete_fs_inst "List.char" (thm "perm_char_def")
  22.185 -         |> discrete_cp_inst "List.char" (thm "perm_char_def")
  22.186 +         |> discrete_pt_inst "nat"  @{thm "perm_nat_def"}
  22.187 +         |> discrete_fs_inst "nat"  @{thm "perm_nat_def"}
  22.188 +         |> discrete_cp_inst "nat"  @{thm "perm_nat_def"}
  22.189 +         |> discrete_pt_inst "bool" @{thm "perm_bool"}
  22.190 +         |> discrete_fs_inst "bool" @{thm "perm_bool"}
  22.191 +         |> discrete_cp_inst "bool" @{thm "perm_bool"}
  22.192 +         |> discrete_pt_inst "IntDef.int" @{thm "perm_int_def"}
  22.193 +         |> discrete_fs_inst "IntDef.int" @{thm "perm_int_def"}
  22.194 +         |> discrete_cp_inst "IntDef.int" @{thm "perm_int_def"}
  22.195 +         |> discrete_pt_inst "List.char" @{thm "perm_char_def"}
  22.196 +         |> discrete_fs_inst "List.char" @{thm "perm_char_def"}
  22.197 +         |> discrete_cp_inst "List.char" @{thm "perm_char_def"}
  22.198          end;
  22.199  
  22.200  
  22.201         (* abbreviations for some lemmas *)
  22.202         (*===============================*)
  22.203 -       val abs_fun_pi          = thm "Nominal.abs_fun_pi";
  22.204 -       val abs_fun_pi_ineq     = thm "Nominal.abs_fun_pi_ineq";
  22.205 -       val abs_fun_eq          = thm "Nominal.abs_fun_eq";
  22.206 -       val abs_fun_eq'         = thm "Nominal.abs_fun_eq'";
  22.207 -       val abs_fun_fresh       = thm "Nominal.abs_fun_fresh";
  22.208 -       val abs_fun_fresh'      = thm "Nominal.abs_fun_fresh'";
  22.209 -       val dj_perm_forget      = thm "Nominal.dj_perm_forget";
  22.210 -       val dj_pp_forget        = thm "Nominal.dj_perm_perm_forget";
  22.211 -       val fresh_iff           = thm "Nominal.fresh_abs_fun_iff";
  22.212 -       val fresh_iff_ineq      = thm "Nominal.fresh_abs_fun_iff_ineq";
  22.213 -       val abs_fun_supp        = thm "Nominal.abs_fun_supp";
  22.214 -       val abs_fun_supp_ineq   = thm "Nominal.abs_fun_supp_ineq";
  22.215 -       val pt_swap_bij         = thm "Nominal.pt_swap_bij";
  22.216 -       val pt_swap_bij'        = thm "Nominal.pt_swap_bij'";
  22.217 -       val pt_fresh_fresh      = thm "Nominal.pt_fresh_fresh";
  22.218 -       val pt_bij              = thm "Nominal.pt_bij";
  22.219 -       val pt_perm_compose     = thm "Nominal.pt_perm_compose";
  22.220 -       val pt_perm_compose'    = thm "Nominal.pt_perm_compose'";
  22.221 -       val perm_app            = thm "Nominal.pt_fun_app_eq";
  22.222 -       val at_fresh            = thm "Nominal.at_fresh";
  22.223 -       val at_fresh_ineq       = thm "Nominal.at_fresh_ineq";
  22.224 -       val at_calc             = thms "Nominal.at_calc";
  22.225 -       val at_swap_simps       = thms "Nominal.at_swap_simps";
  22.226 -       val at_supp             = thm "Nominal.at_supp";
  22.227 -       val dj_supp             = thm "Nominal.dj_supp";
  22.228 -       val fresh_left_ineq     = thm "Nominal.pt_fresh_left_ineq";
  22.229 -       val fresh_left          = thm "Nominal.pt_fresh_left";
  22.230 -       val fresh_right_ineq    = thm "Nominal.pt_fresh_right_ineq";
  22.231 -       val fresh_right         = thm "Nominal.pt_fresh_right";
  22.232 -       val fresh_bij_ineq      = thm "Nominal.pt_fresh_bij_ineq";
  22.233 -       val fresh_bij           = thm "Nominal.pt_fresh_bij";
  22.234 -       val fresh_eqvt          = thm "Nominal.pt_fresh_eqvt";
  22.235 -       val fresh_eqvt_ineq     = thm "Nominal.pt_fresh_eqvt_ineq";
  22.236 -       val set_diff_eqvt       = thm "Nominal.pt_set_diff_eqvt";
  22.237 -       val in_eqvt             = thm "Nominal.pt_in_eqvt";
  22.238 -       val eq_eqvt             = thm "Nominal.pt_eq_eqvt";
  22.239 -       val all_eqvt            = thm "Nominal.pt_all_eqvt";
  22.240 -       val ex_eqvt             = thm "Nominal.pt_ex_eqvt";
  22.241 -       val pt_pi_rev           = thm "Nominal.pt_pi_rev";
  22.242 -       val pt_rev_pi           = thm "Nominal.pt_rev_pi";
  22.243 -       val at_exists_fresh     = thm "Nominal.at_exists_fresh";
  22.244 -       val at_exists_fresh'    = thm "Nominal.at_exists_fresh'";
  22.245 -       val fresh_perm_app_ineq = thm "Nominal.pt_fresh_perm_app_ineq";
  22.246 -       val fresh_perm_app      = thm "Nominal.pt_fresh_perm_app";	
  22.247 -       val fresh_aux           = thm "Nominal.pt_fresh_aux";  
  22.248 -       val pt_perm_supp_ineq   = thm "Nominal.pt_perm_supp_ineq";
  22.249 -       val pt_perm_supp        = thm "Nominal.pt_perm_supp";
  22.250 +       val abs_fun_pi          = @{thm "Nominal.abs_fun_pi"};
  22.251 +       val abs_fun_pi_ineq     = @{thm "Nominal.abs_fun_pi_ineq"};
  22.252 +       val abs_fun_eq          = @{thm "Nominal.abs_fun_eq"};
  22.253 +       val abs_fun_eq'         = @{thm "Nominal.abs_fun_eq'"};
  22.254 +       val abs_fun_fresh       = @{thm "Nominal.abs_fun_fresh"};
  22.255 +       val abs_fun_fresh'      = @{thm "Nominal.abs_fun_fresh'"};
  22.256 +       val dj_perm_forget      = @{thm "Nominal.dj_perm_forget"};
  22.257 +       val dj_pp_forget        = @{thm "Nominal.dj_perm_perm_forget"};
  22.258 +       val fresh_iff           = @{thm "Nominal.fresh_abs_fun_iff"};
  22.259 +       val fresh_iff_ineq      = @{thm "Nominal.fresh_abs_fun_iff_ineq"};
  22.260 +       val abs_fun_supp        = @{thm "Nominal.abs_fun_supp"};
  22.261 +       val abs_fun_supp_ineq   = @{thm "Nominal.abs_fun_supp_ineq"};
  22.262 +       val pt_swap_bij         = @{thm "Nominal.pt_swap_bij"};
  22.263 +       val pt_swap_bij'        = @{thm "Nominal.pt_swap_bij'"};
  22.264 +       val pt_fresh_fresh      = @{thm "Nominal.pt_fresh_fresh"};
  22.265 +       val pt_bij              = @{thm "Nominal.pt_bij"};
  22.266 +       val pt_perm_compose     = @{thm "Nominal.pt_perm_compose"};
  22.267 +       val pt_perm_compose'    = @{thm "Nominal.pt_perm_compose'"};
  22.268 +       val perm_app            = @{thm "Nominal.pt_fun_app_eq"};
  22.269 +       val at_fresh            = @{thm "Nominal.at_fresh"};
  22.270 +       val at_fresh_ineq       = @{thm "Nominal.at_fresh_ineq"};
  22.271 +       val at_calc             = @{thms "Nominal.at_calc"};
  22.272 +       val at_swap_simps       = @{thms "Nominal.at_swap_simps"};
  22.273 +       val at_supp             = @{thm "Nominal.at_supp"};
  22.274 +       val dj_supp             = @{thm "Nominal.dj_supp"};
  22.275 +       val fresh_left_ineq     = @{thm "Nominal.pt_fresh_left_ineq"};
  22.276 +       val fresh_left          = @{thm "Nominal.pt_fresh_left"};
  22.277 +       val fresh_right_ineq    = @{thm "Nominal.pt_fresh_right_ineq"};
  22.278 +       val fresh_right         = @{thm "Nominal.pt_fresh_right"};
  22.279 +       val fresh_bij_ineq      = @{thm "Nominal.pt_fresh_bij_ineq"};
  22.280 +       val fresh_bij           = @{thm "Nominal.pt_fresh_bij"};
  22.281 +       val fresh_eqvt          = @{thm "Nominal.pt_fresh_eqvt"};
  22.282 +       val fresh_eqvt_ineq     = @{thm "Nominal.pt_fresh_eqvt_ineq"};
  22.283 +       val set_diff_eqvt       = @{thm "Nominal.pt_set_diff_eqvt"};
  22.284 +       val in_eqvt             = @{thm "Nominal.pt_in_eqvt"};
  22.285 +       val eq_eqvt             = @{thm "Nominal.pt_eq_eqvt"};
  22.286 +       val all_eqvt            = @{thm "Nominal.pt_all_eqvt"};
  22.287 +       val ex_eqvt             = @{thm "Nominal.pt_ex_eqvt"};
  22.288 +       val pt_pi_rev           = @{thm "Nominal.pt_pi_rev"};
  22.289 +       val pt_rev_pi           = @{thm "Nominal.pt_rev_pi"};
  22.290 +       val at_exists_fresh     = @{thm "Nominal.at_exists_fresh"};
  22.291 +       val at_exists_fresh'    = @{thm "Nominal.at_exists_fresh'"};
  22.292 +       val fresh_perm_app_ineq = @{thm "Nominal.pt_fresh_perm_app_ineq"};
  22.293 +       val fresh_perm_app      = @{thm "Nominal.pt_fresh_perm_app"};	
  22.294 +       val fresh_aux           = @{thm "Nominal.pt_fresh_aux"};  
  22.295 +       val pt_perm_supp_ineq   = @{thm "Nominal.pt_perm_supp_ineq"};
  22.296 +       val pt_perm_supp        = @{thm "Nominal.pt_perm_supp"};
  22.297  
  22.298         (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
  22.299         (* types; this allows for example to use abs_perm (which is a      *)

    23.1 --- a/src/HOL/NumberTheory/Chinese.thy	Sat Jul 21 17:40:40 2007 +0200
    23.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Sat Jul 21 23:25:00 2007 +0200
    23.3 @@ -246,7 +246,7 @@
    23.4           prefer 7
    23.5           apply (simp add: zmult_ac)
    23.6          apply (unfold xilin_sol_def)
    23.7 -        apply (tactic {* Asm_simp_tac 7 *})
    23.8 +        apply (tactic {* asm_simp_tac @{simpset} 7 *})
    23.9          apply (rule_tac [7] ex1_implies_ex [THEN someI_ex])
   23.10          apply (rule_tac [7] unique_xi_sol)
   23.11             apply (rule_tac [4] funprod_zdvd)

    24.1 --- a/src/HOL/NumberTheory/WilsonBij.thy	Sat Jul 21 17:40:40 2007 +0200
    24.2 +++ b/src/HOL/NumberTheory/WilsonBij.thy	Sat Jul 21 23:25:00 2007 +0200
    24.3 @@ -150,7 +150,7 @@
    24.4          apply (rule_tac [7] zcong_trans)
    24.5           apply (tactic {* stac (thm "zcong_sym") 8 *})
    24.6           apply (erule_tac [7] inv_is_inv)
    24.7 -          apply (tactic "Asm_simp_tac 9")
    24.8 +          apply (tactic "asm_simp_tac @{simpset} 9")
    24.9            apply (erule_tac [9] inv_is_inv)
   24.10             apply (rule_tac [6] zless_zprime_imp_zrelprime)
   24.11               apply (rule_tac [8] inv_less)

    25.1 --- a/src/HOL/NumberTheory/WilsonRuss.thy	Sat Jul 21 17:40:40 2007 +0200
    25.2 +++ b/src/HOL/NumberTheory/WilsonRuss.thy	Sat Jul 21 23:25:00 2007 +0200
    25.3 @@ -270,7 +270,7 @@
    25.4         apply (simp add: zmult_assoc)
    25.5        apply (rule_tac [5] zcong_zmult)
    25.6         apply (rule_tac [5] inv_is_inv)
    25.7 -         apply (tactic "Clarify_tac 4")
    25.8 +         apply (tactic "clarify_tac @{claset} 4")
    25.9           apply (subgoal_tac [4] "a \<in> wset (a - 1, p)")
   25.10            apply (rule_tac [5] wset_inv_mem_mem)
   25.11                 apply (simp_all add: wset_fin)

    26.1 --- a/src/HOL/ROOT.ML	Sat Jul 21 17:40:40 2007 +0200
    26.2 +++ b/src/HOL/ROOT.ML	Sat Jul 21 23:25:00 2007 +0200
    26.3 @@ -7,5 +7,3 @@
    26.4  use_thy "Main";
    26.5  
    26.6  path_add "~~/src/HOL/Library";
    26.7 -
    26.8 -Goal "True";  (*leave subgoal package empty*)

    27.1 --- a/src/HOL/Tools/meson.ML	Sat Jul 21 17:40:40 2007 +0200
    27.2 +++ b/src/HOL/Tools/meson.ML	Sat Jul 21 23:25:00 2007 +0200
    27.3 @@ -575,7 +575,7 @@
    27.4  
    27.5  (*First, breaks the goal into independent units*)
    27.6  val safe_best_meson_tac =
    27.7 -     SELECT_GOAL (TRY Safe_tac THEN
    27.8 +     SELECT_GOAL (TRY (CLASET safe_tac) THEN
    27.9                    TRYALL (best_meson_tac size_of_subgoals));
   27.10  
   27.11  (** Depth-first search version **)

    28.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Sat Jul 21 17:40:40 2007 +0200
    28.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Sat Jul 21 23:25:00 2007 +0200
    28.3 @@ -195,7 +195,7 @@
    28.4        val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args));
    28.5      in Library.foldr mk_ex (vns, conj) end;
    28.6  
    28.7 -  val conj_assoc = thm "conj_assoc";
    28.8 +  val conj_assoc = @{thm conj_assoc};
    28.9    val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons);
   28.10    val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start;
   28.11    val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1;
   28.12 @@ -333,7 +333,7 @@
   28.13  end;
   28.14  
   28.15  local
   28.16 -  val rev_contrapos = thm "rev_contrapos";
   28.17 +  val rev_contrapos = @{thm rev_contrapos};
   28.18    fun con_strict (con, args) = 
   28.19      let
   28.20        fun one_strict vn =
   28.21 @@ -441,7 +441,7 @@
   28.22  end;
   28.23  
   28.24  val sel_rews = sel_stricts @ sel_defins @ sel_apps;
   28.25 -val rev_contrapos = thm "rev_contrapos";
   28.26 +val rev_contrapos = @{thm rev_contrapos};
   28.27  
   28.28  val distincts_le =
   28.29    let

    29.1 --- a/src/ZF/ROOT.ML	Sat Jul 21 17:40:40 2007 +0200
    29.2 +++ b/src/ZF/ROOT.ML	Sat Jul 21 23:25:00 2007 +0200
    29.3 @@ -12,5 +12,3 @@
    29.4  writeln banner;
    29.5  
    29.6  use_thy "Main_ZFC";
    29.7 -
    29.8 -Goal "True";  (*leave subgoal package empty*)

    30.1 --- a/src/ZF/UNITY/Constrains.thy	Sat Jul 21 17:40:40 2007 +0200
    30.2 +++ b/src/ZF/UNITY/Constrains.thy	Sat Jul 21 23:25:00 2007 +0200
    30.3 @@ -537,7 +537,8 @@
    30.4  
    30.5  (*proves "co" properties when the program is specified*)
    30.6  
    30.7 -fun gen_constrains_tac(cs,ss) i = 
    30.8 +fun constrains_tac ctxt =
    30.9 +  let val css as (cs, ss) = local_clasimpset_of ctxt in
   30.10     SELECT_GOAL
   30.11        (EVERY [REPEAT (Always_Int_tac 1),
   30.12                REPEAT (etac Always_ConstrainsI 1
   30.13 @@ -547,27 +548,30 @@
   30.14                rtac constrainsI 1,
   30.15                (* Three subgoals *)
   30.16                rewrite_goal_tac [st_set_def] 3,
   30.17 -              REPEAT (Force_tac 2),
   30.18 +              REPEAT (force_tac css 2),
   30.19                full_simp_tac (ss addsimps !program_defs_ref) 1,
   30.20                ALLGOALS (clarify_tac cs),
   30.21                REPEAT (FIRSTGOAL (etac disjE)),
   30.22 -              ALLGOALS Clarify_tac,
   30.23 +              ALLGOALS (clarify_tac cs),
   30.24                REPEAT (FIRSTGOAL (etac disjE)),
   30.25                ALLGOALS (clarify_tac cs),
   30.26                ALLGOALS (asm_full_simp_tac ss),
   30.27 -              ALLGOALS (clarify_tac cs)]) i;
   30.28 -
   30.29 -fun constrains_tac st = gen_constrains_tac (claset(), simpset()) st;
   30.30 +              ALLGOALS (clarify_tac cs)])
   30.31 +  end;
   30.32  
   30.33  (*For proving invariants*)
   30.34 -fun always_tac i = 
   30.35 -    rtac AlwaysI i THEN Force_tac i THEN constrains_tac i;
   30.36 +fun always_tac ctxt i = 
   30.37 +    rtac AlwaysI i THEN force_tac (local_clasimpset_of ctxt) i THEN constrains_tac ctxt i;
   30.38  *}
   30.39  
   30.40  method_setup safety = {*
   30.41    Method.ctxt_args (fn ctxt =>
   30.42 -    Method.SIMPLE_METHOD' (gen_constrains_tac (local_clasimpset_of ctxt))) *}
   30.43 +    Method.SIMPLE_METHOD' (constrains_tac ctxt)) *}
   30.44    "for proving safety properties"
   30.45  
   30.46 +method_setup always = {*
   30.47 +  Method.ctxt_args (fn ctxt =>
   30.48 +    Method.SIMPLE_METHOD' (always_tac ctxt)) *}
   30.49 +  "for proving invariants"
   30.50  
   30.51  end

    31.1 --- a/src/ZF/UNITY/SubstAx.thy	Sat Jul 21 17:40:40 2007 +0200
    31.2 +++ b/src/ZF/UNITY/SubstAx.thy	Sat Jul 21 23:25:00 2007 +0200
    31.3 @@ -403,7 +403,8 @@
    31.4  
    31.5  
    31.6  (*proves "ensures/leadsTo" properties when the program is specified*)
    31.7 -fun gen_ensures_tac(cs,ss) sact = 
    31.8 +fun ensures_tac ctxt sact =
    31.9 +  let val css as (cs, ss) = local_clasimpset_of ctxt in
   31.10      SELECT_GOAL
   31.11        (EVERY [REPEAT (Always_Int_tac 1),
   31.12                etac Always_LeadsTo_Basis 1 
   31.13 @@ -416,26 +417,22 @@
   31.14                   (*simplify the command's domain*)
   31.15                simp_tac (ss addsimps [domain_def]) 3, 
   31.16                (* proving the domain part *)
   31.17 -             clarify_tac cs 3, dtac Cla.swap 3, force_tac (cs,ss) 4,
   31.18 -             rtac ReplaceI 3, force_tac (cs,ss) 3, force_tac (cs,ss) 4,
   31.19 +             clarify_tac cs 3, dtac Cla.swap 3, force_tac css 4,
   31.20 +             rtac ReplaceI 3, force_tac css 3, force_tac css 4,
   31.21               asm_full_simp_tac ss 3, rtac conjI 3, simp_tac ss 4,
   31.22               REPEAT (rtac state_update_type 3),
   31.23 -             gen_constrains_tac (cs,ss) 1,
   31.24 +             constrains_tac ctxt 1,
   31.25               ALLGOALS (clarify_tac cs),
   31.26               ALLGOALS (asm_full_simp_tac (ss addsimps [st_set_def])),
   31.27                          ALLGOALS (clarify_tac cs),
   31.28 -            ALLGOALS (asm_lr_simp_tac ss)]);
   31.29 -
   31.30 -fun ensures_tac sact = gen_ensures_tac (claset(), simpset()) sact;
   31.31 +            ALLGOALS (asm_lr_simp_tac ss)])
   31.32 +  end;
   31.33  *}
   31.34  
   31.35 -
   31.36  method_setup ensures_tac = {*
   31.37      fn args => fn ctxt =>
   31.38 -        Method.goal_args' (Scan.lift Args.name) 
   31.39 -           (gen_ensures_tac (local_clasimpset_of ctxt))
   31.40 +        Method.goal_args' (Scan.lift Args.name) (ensures_tac ctxt)
   31.41             args ctxt *}
   31.42      "for proving progress properties"
   31.43  
   31.44 -
   31.45  end