eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
authorwenzelm
Fri Mar 20 15:24:18 2009 +0100 (2009-03-20)
changeset 30607c3d1590debd8
parent 30606 40a1865ab122
child 30608 d9805c5b5d2e
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
doc-src/TutorialI/Protocol/Message.thy
doc-src/TutorialI/Protocol/Public.thy
src/CCL/Type.thy
src/HOL/Auth/Message.thy
src/HOL/IMPP/Hoare.thy
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/SET-Protocol/Cardholder_Registration.thy
src/HOL/SET-Protocol/MessageSET.thy
src/HOL/SET-Protocol/PublicSET.thy
src/HOL/SET-Protocol/Purchase.thy
src/HOL/SizeChange/sct.ML
src/HOL/Tools/cnf_funcs.ML
src/HOL/Tools/function_package/fundef_core.ML
src/HOL/Tools/function_package/mutual.ML
src/HOL/Tools/function_package/scnp_reconstruct.ML
src/HOL/Tools/function_package/termination.ML
src/HOL/Tools/meson.ML
src/HOL/Word/WordArith.thy
src/HOL/ex/Classical.thy
src/HOLCF/IOA/ex/TrivEx.thy
src/HOLCF/IOA/ex/TrivEx2.thy
src/HOLCF/IOA/meta_theory/Abstraction.thy
src/HOLCF/IOA/meta_theory/Sequence.thy
src/HOLCF/IOA/meta_theory/Traces.thy
src/HOLCF/Lift.thy
src/Sequents/LK.thy
src/ZF/int_arith.ML
     1.1 --- a/doc-src/TutorialI/Protocol/Message.thy	Fri Mar 20 11:26:59 2009 +0100
     1.2 +++ b/doc-src/TutorialI/Protocol/Message.thy	Fri Mar 20 15:24:18 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Auth/Message
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   1996  University of Cambridge
     1.8  
     1.9 @@ -830,9 +829,9 @@
    1.10  (*Prove base case (subgoal i) and simplify others.  A typical base case
    1.11    concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
    1.12    alone.*)
    1.13 -fun prove_simple_subgoals_tac i = 
    1.14 -    force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN
    1.15 -    ALLGOALS Asm_simp_tac
    1.16 +fun prove_simple_subgoals_tac (cs, ss) i = 
    1.17 +    force_tac (cs, ss addsimps [@{thm image_eq_UN}]) i THEN
    1.18 +    ALLGOALS (asm_simp_tac ss)
    1.19  
    1.20  (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
    1.21    but this application is no longer necessary if analz_insert_eq is used.
    1.22 @@ -857,8 +856,7 @@
    1.23  		  (cs addIs [analz_insertI,
    1.24  				   impOfSubs analz_subset_parts]) 4 1))
    1.25  
    1.26 -(*The explicit claset and simpset arguments help it work with Isar*)
    1.27 -fun gen_spy_analz_tac (cs,ss) i =
    1.28 +fun spy_analz_tac (cs,ss) i =
    1.29    DETERM
    1.30     (SELECT_GOAL
    1.31       (EVERY 
    1.32 @@ -870,8 +868,6 @@
    1.33         simp_tac ss 1,
    1.34         REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
    1.35         DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
    1.36 -
    1.37 -fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
    1.38  *}
    1.39  
    1.40  text{*By default only @{text o_apply} is built-in.  But in the presence of
    1.41 @@ -919,7 +915,7 @@
    1.42  lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
    1.43  
    1.44  method_setup spy_analz = {*
    1.45 -    Scan.succeed (SIMPLE_METHOD' o gen_spy_analz_tac o local_clasimpset_of) *}
    1.46 +    Scan.succeed (SIMPLE_METHOD' o spy_analz_tac o local_clasimpset_of) *}
    1.47      "for proving the Fake case when analz is involved"
    1.48  
    1.49  method_setup atomic_spy_analz = {*
     2.1 --- a/doc-src/TutorialI/Protocol/Public.thy	Fri Mar 20 11:26:59 2009 +0100
     2.2 +++ b/doc-src/TutorialI/Protocol/Public.thy	Fri Mar 20 15:24:18 2009 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      HOL/Auth/Public
     2.5 -    ID:         $Id$
     2.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7      Copyright   1996  University of Cambridge
     2.8  
     2.9 @@ -153,15 +152,15 @@
    2.10  
    2.11  (*Tactic for possibility theorems*)
    2.12  ML {*
    2.13 -fun possibility_tac st = st |>
    2.14 +fun possibility ctxt =
    2.15      REPEAT (*omit used_Says so that Nonces start from different traces!*)
    2.16 -    (ALLGOALS (simp_tac (@{simpset} delsimps [used_Says]))
    2.17 +    (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says]))
    2.18       THEN
    2.19       REPEAT_FIRST (eq_assume_tac ORELSE' 
    2.20                     resolve_tac [refl, conjI, @{thm Nonce_supply}]));
    2.21  *}
    2.22  
    2.23 -method_setup possibility = {* Scan.succeed (K (SIMPLE_METHOD possibility_tac)) *}
    2.24 +method_setup possibility = {* Scan.succeed (SIMPLE_METHOD o possibility_tac) *}
    2.25      "for proving possibility theorems"
    2.26  
    2.27  end
     3.1 --- a/src/CCL/Type.thy	Fri Mar 20 11:26:59 2009 +0100
     3.2 +++ b/src/CCL/Type.thy	Fri Mar 20 15:24:18 2009 +0100
     3.3 @@ -1,5 +1,4 @@
     3.4  (*  Title:      CCL/Type.thy
     3.5 -    ID:         $Id$
     3.6      Author:     Martin Coen
     3.7      Copyright   1993  University of Cambridge
     3.8  *)
     3.9 @@ -409,7 +408,7 @@
    3.10  
    3.11  fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s
    3.12        (fn prems => [rtac (genXH RS iffD2) 1,
    3.13 -                    SIMPSET' simp_tac 1,
    3.14 +                    simp_tac (simpset_of thy) 1,
    3.15                      TRY (fast_tac (@{claset} addIs
    3.16                              ([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI]
    3.17                               @ prems)) 1)])
    3.18 @@ -442,8 +441,8 @@
    3.19     "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))",
    3.20     "[| <h,h'> : lfp(%x. POgen(x) Un R Un PO);  <t,t'> : lfp(%x. POgen(x) Un R Un PO) |] ==> <h$t,h'$t'> : POgen(lfp(%x. POgen(x) Un R Un PO))"];
    3.21  
    3.22 -fun POgen_tac (rla,rlb) i =
    3.23 -  SELECT_GOAL (CLASET safe_tac) i THEN
    3.24 +fun POgen_tac ctxt (rla,rlb) i =
    3.25 +  SELECT_GOAL (safe_tac (local_claset_of ctxt)) i THEN
    3.26    rtac (rlb RS (rla RS (thm "ssubst_pair"))) i THEN
    3.27    (REPEAT (resolve_tac (POgenIs @ [thm "PO_refl" RS (thm "POgen_mono" RS ci3_AI)] @
    3.28      (POgenIs RL [thm "POgen_mono" RS ci3_AgenI]) @ [thm "POgen_mono" RS ci3_RI]) i));
     4.1 --- a/src/HOL/Auth/Message.thy	Fri Mar 20 11:26:59 2009 +0100
     4.2 +++ b/src/HOL/Auth/Message.thy	Fri Mar 20 15:24:18 2009 +0100
     4.3 @@ -1,5 +1,4 @@
     4.4  (*  Title:      HOL/Auth/Message
     4.5 -    ID:         $Id$
     4.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7      Copyright   1996  University of Cambridge
     4.8  
     4.9 @@ -848,9 +847,9 @@
    4.10  (*Prove base case (subgoal i) and simplify others.  A typical base case
    4.11    concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
    4.12    alone.*)
    4.13 -fun prove_simple_subgoals_tac i = 
    4.14 -    CLASIMPSET' (fn (cs, ss) => force_tac (cs, ss addsimps [@{thm image_eq_UN}])) i THEN
    4.15 -    ALLGOALS (SIMPSET' asm_simp_tac)
    4.16 +fun prove_simple_subgoals_tac (cs, ss) i = 
    4.17 +    force_tac (cs, ss addsimps [@{thm image_eq_UN}]) i THEN
    4.18 +    ALLGOALS (asm_simp_tac ss)
    4.19  
    4.20  (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
    4.21    but this application is no longer necessary if analz_insert_eq is used.
    4.22 @@ -875,8 +874,7 @@
    4.23  		  (cs addIs [@{thm analz_insertI},
    4.24  				   impOfSubs @{thm analz_subset_parts}]) 4 1))
    4.25  
    4.26 -(*The explicit claset and simpset arguments help it work with Isar*)
    4.27 -fun gen_spy_analz_tac (cs,ss) i =
    4.28 +fun spy_analz_tac (cs,ss) i =
    4.29    DETERM
    4.30     (SELECT_GOAL
    4.31       (EVERY 
    4.32 @@ -888,8 +886,6 @@
    4.33         REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
    4.34         DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
    4.35  
    4.36 -val spy_analz_tac = CLASIMPSET' gen_spy_analz_tac;
    4.37 -
    4.38  end
    4.39  *}
    4.40  
    4.41 @@ -941,7 +937,7 @@
    4.42  lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
    4.43  
    4.44  method_setup spy_analz = {*
    4.45 -    Scan.succeed (SIMPLE_METHOD' o Message.gen_spy_analz_tac o local_clasimpset_of) *}
    4.46 +    Scan.succeed (SIMPLE_METHOD' o Message.spy_analz_tac o local_clasimpset_of) *}
    4.47      "for proving the Fake case when analz is involved"
    4.48  
    4.49  method_setup atomic_spy_analz = {*
     5.1 --- a/src/HOL/IMPP/Hoare.thy	Fri Mar 20 11:26:59 2009 +0100
     5.2 +++ b/src/HOL/IMPP/Hoare.thy	Fri Mar 20 15:24:18 2009 +0100
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      HOL/IMPP/Hoare.thy
     5.5 -    ID:         $Id$
     5.6      Author:     David von Oheimb
     5.7      Copyright   1999 TUM
     5.8  *)
     5.9 @@ -219,7 +218,7 @@
    5.10  apply           (rule hoare_derivs.conseq, intro strip, tactic "smp_tac 2 1", clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI)
    5.11  prefer 7
    5.12  apply          (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast)
    5.13 -apply         (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) (thms "hoare_derivs.intros")) THEN_ALL_NEW CLASET' fast_tac) *})
    5.14 +apply         (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) (thms "hoare_derivs.intros")) THEN_ALL_NEW (fast_tac @{claset})) *})
    5.15  done
    5.16  
    5.17  lemma weak_Body: "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}"
    5.18 @@ -291,7 +290,7 @@
    5.19     simp_tac @{simpset}, clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
    5.20  apply       (simp_all (no_asm_use) add: triple_valid_def2)
    5.21  apply       (intro strip, tactic "smp_tac 2 1", blast) (* conseq *)
    5.22 -apply      (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *}) (* Skip, Ass, Local *)
    5.23 +apply      (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *}) (* Skip, Ass, Local *)
    5.24  prefer 3 apply   (force) (* Call *)
    5.25  apply  (erule_tac [2] evaln_elim_cases) (* If *)
    5.26  apply   blast+
    5.27 @@ -336,17 +335,17 @@
    5.28  lemma MGF_lemma1 [rule_format (no_asm)]: "state_not_singleton ==>  
    5.29    !pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}"
    5.30  apply (induct_tac c)
    5.31 -apply        (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *})
    5.32 +apply        (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *})
    5.33  prefer 7 apply        (fast intro: domI)
    5.34  apply (erule_tac [6] MGT_alternD)
    5.35  apply       (unfold MGT_def)
    5.36  apply       (drule_tac [7] bspec, erule_tac [7] domI)
    5.37 -apply       (rule_tac [7] escape, tactic {* CLASIMPSET' clarsimp_tac 7 *},
    5.38 +apply       (rule_tac [7] escape, tactic {* clarsimp_tac @{clasimpset} 7 *},
    5.39    rule_tac [7] P1 = "%Z' s. s= (setlocs Z newlocs) [Loc Arg ::= fun Z]" in hoare_derivs.Call [THEN conseq1], erule_tac [7] conseq12)
    5.40  apply        (erule_tac [!] thin_rl)
    5.41  apply (rule hoare_derivs.Skip [THEN conseq2])
    5.42  apply (rule_tac [2] hoare_derivs.Ass [THEN conseq1])
    5.43 -apply        (rule_tac [3] escape, tactic {* CLASIMPSET' clarsimp_tac 3 *},
    5.44 +apply        (rule_tac [3] escape, tactic {* clarsimp_tac @{clasimpset} 3 *},
    5.45    rule_tac [3] P1 = "%Z' s. s= (Z[Loc loc::=fun Z])" in hoare_derivs.Local [THEN conseq1],
    5.46    erule_tac [3] conseq12)
    5.47  apply         (erule_tac [5] hoare_derivs.Comp, erule_tac [5] conseq12)
    5.48 @@ -365,7 +364,7 @@
    5.49    shows "finite U ==> uG = mgt_call`U ==>  
    5.50    !G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})"
    5.51  apply (induct_tac n)
    5.52 -apply  (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *})
    5.53 +apply  (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *})
    5.54  apply  (subgoal_tac "G = mgt_call ` U")
    5.55  prefer 2
    5.56  apply   (simp add: card_seteq finite_imageI)
     6.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Fri Mar 20 11:26:59 2009 +0100
     6.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Fri Mar 20 15:24:18 2009 +0100
     6.3 @@ -109,7 +109,7 @@
     6.4  (
     6.5  OldGoals.push_proof();
     6.6  OldGoals.goalw_cterm [] (cterm_of sign trm);
     6.7 -by (SIMPSET' simp_tac 1);
     6.8 +by (simp_tac (simpset_of sign) 1);
     6.9          let
    6.10          val if_tmp_result = result()
    6.11          in
     7.1 --- a/src/HOL/SET-Protocol/Cardholder_Registration.thy	Fri Mar 20 11:26:59 2009 +0100
     7.2 +++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy	Fri Mar 20 15:24:18 2009 +0100
     7.3 @@ -1,5 +1,4 @@
     7.4  (*  Title:      HOL/Auth/SET/Cardholder_Registration
     7.5 -    ID:         $Id$
     7.6      Authors:    Giampaolo Bella, Fabio Massacci, Lawrence C Paulson,
     7.7                  Piero Tramontano
     7.8  *)
     7.9 @@ -263,7 +262,7 @@
    7.10  	 THEN set_cr.SET_CR5 [of concl: C i KC3 NC3 KC2 CardSecret],
    7.11  	 THEN Says_to_Gets,  
    7.12  	 THEN set_cr.SET_CR6 [of concl: i C KC2]])
    7.13 -apply (tactic "PublicSET.basic_possibility_tac")
    7.14 +apply basic_possibility
    7.15  apply (simp_all (no_asm_simp) add: symKeys_neq_imp_neq)
    7.16  done
    7.17  
     8.1 --- a/src/HOL/SET-Protocol/MessageSET.thy	Fri Mar 20 11:26:59 2009 +0100
     8.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy	Fri Mar 20 15:24:18 2009 +0100
     8.3 @@ -1,5 +1,4 @@
     8.4  (*  Title:      HOL/Auth/SET/MessageSET
     8.5 -    ID:         $Id$
     8.6      Authors:     Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
     8.7  *)
     8.8  
     8.9 @@ -846,9 +845,9 @@
    8.10  (*Prove base case (subgoal i) and simplify others.  A typical base case
    8.11    concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
    8.12    alone.*)
    8.13 -fun prove_simple_subgoals_tac i =
    8.14 -    CLASIMPSET' (fn (cs, ss) => force_tac (cs, ss addsimps [@{thm image_eq_UN}])) i THEN
    8.15 -    ALLGOALS (SIMPSET' asm_simp_tac)
    8.16 +fun prove_simple_subgoals_tac (cs, ss) i =
    8.17 +    force_tac (cs, ss addsimps [@{thm image_eq_UN}]) i THEN
    8.18 +    ALLGOALS (asm_simp_tac ss)
    8.19  
    8.20  (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
    8.21    but this application is no longer necessary if analz_insert_eq is used.
    8.22 @@ -873,8 +872,7 @@
    8.23  		  (cs addIs [@{thm analz_insertI},
    8.24  				   impOfSubs @{thm analz_subset_parts}]) 4 1))
    8.25  
    8.26 -(*The explicit claset and simpset arguments help it work with Isar*)
    8.27 -fun gen_spy_analz_tac (cs,ss) i =
    8.28 +fun spy_analz_tac (cs,ss) i =
    8.29    DETERM
    8.30     (SELECT_GOAL
    8.31       (EVERY
    8.32 @@ -887,8 +885,6 @@
    8.33         REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
    8.34         DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
    8.35  
    8.36 -val spy_analz_tac = CLASIMPSET' gen_spy_analz_tac;
    8.37 -
    8.38  end
    8.39  *}
    8.40  (*>*)
    8.41 @@ -941,7 +937,7 @@
    8.42  
    8.43  method_setup spy_analz = {*
    8.44      Scan.succeed (fn ctxt =>
    8.45 -        SIMPLE_METHOD' (MessageSET.gen_spy_analz_tac (local_clasimpset_of ctxt))) *}
    8.46 +        SIMPLE_METHOD' (MessageSET.spy_analz_tac (local_clasimpset_of ctxt))) *}
    8.47      "for proving the Fake case when analz is involved"
    8.48  
    8.49  method_setup atomic_spy_analz = {*
     9.1 --- a/src/HOL/SET-Protocol/PublicSET.thy	Fri Mar 20 11:26:59 2009 +0100
     9.2 +++ b/src/HOL/SET-Protocol/PublicSET.thy	Fri Mar 20 15:24:18 2009 +0100
     9.3 @@ -1,6 +1,5 @@
     9.4  (*  Title:      HOL/Auth/SET/PublicSET
     9.5 -    ID:         $Id$
     9.6 -    Authors:     Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
     9.7 +    Authors:    Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
     9.8  *)
     9.9  
    9.10  header{*The Public-Key Theory, Modified for SET*}
    9.11 @@ -348,22 +347,19 @@
    9.12  structure PublicSET =
    9.13  struct
    9.14  
    9.15 -(*Tactic for possibility theorems (Isar interface)*)
    9.16 -fun gen_possibility_tac ss state = state |>
    9.17 +(*Tactic for possibility theorems*)
    9.18 +fun possibility_tac ctxt =
    9.19      REPEAT (*omit used_Says so that Nonces start from different traces!*)
    9.20 -    (ALLGOALS (simp_tac (ss delsimps [@{thm used_Says}, @{thm used_Notes}]))
    9.21 +    (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [@{thm used_Says}, @{thm used_Notes}]))
    9.22       THEN
    9.23       REPEAT_FIRST (eq_assume_tac ORELSE' 
    9.24                     resolve_tac [refl, conjI, @{thm Nonce_supply}]))
    9.25  
    9.26 -(*Tactic for possibility theorems (ML script version)*)
    9.27 -fun possibility_tac state = gen_possibility_tac (simpset_of (Thm.theory_of_thm state)) state
    9.28 -
    9.29  (*For harder protocols (such as SET_CR!), where we have to set up some
    9.30    nonces and keys initially*)
    9.31 -fun basic_possibility_tac st = st |>
    9.32 +fun basic_possibility_tac ctxt =
    9.33      REPEAT 
    9.34 -    (ALLGOALS (asm_simp_tac (simpset_of (Thm.theory_of_thm st) setSolver safe_solver))
    9.35 +    (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
    9.36       THEN
    9.37       REPEAT_FIRST (resolve_tac [refl, conjI]))
    9.38  
    9.39 @@ -371,10 +367,12 @@
    9.40  *}
    9.41  
    9.42  method_setup possibility = {*
    9.43 -    Scan.succeed (fn ctxt =>
    9.44 -        SIMPLE_METHOD (PublicSET.gen_possibility_tac (local_simpset_of ctxt))) *}
    9.45 +    Scan.succeed (SIMPLE_METHOD o PublicSET.possibility_tac) *}
    9.46      "for proving possibility theorems"
    9.47  
    9.48 +method_setup basic_possibility = {*
    9.49 +    Scan.succeed (SIMPLE_METHOD o PublicSET.basic_possibility_tac) *}
    9.50 +    "for proving possibility theorems"
    9.51  
    9.52  
    9.53  subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
    10.1 --- a/src/HOL/SET-Protocol/Purchase.thy	Fri Mar 20 11:26:59 2009 +0100
    10.2 +++ b/src/HOL/SET-Protocol/Purchase.thy	Fri Mar 20 15:24:18 2009 +0100
    10.3 @@ -1,5 +1,4 @@
    10.4  (*  Title:      HOL/Auth/SET/Purchase
    10.5 -    ID:         $Id$
    10.6      Authors:    Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
    10.7  *)
    10.8  
    10.9 @@ -335,7 +334,7 @@
   10.10  	  THEN set_pur.AuthResUns [of concl: "PG j" M KP LID_M XID],
   10.11            THEN Says_to_Gets, 
   10.12  	  THEN set_pur.PRes]) 
   10.13 -apply (tactic "PublicSET.basic_possibility_tac")
   10.14 +apply basic_possibility
   10.15  apply (simp_all add: used_Cons symKeys_neq_imp_neq) 
   10.16  done
   10.17  
   10.18 @@ -371,7 +370,7 @@
   10.19  	  THEN set_pur.AuthResS [of concl: "PG j" M KP LID_M XID],
   10.20            THEN Says_to_Gets, 
   10.21  	  THEN set_pur.PRes]) 
   10.22 -apply (tactic "PublicSET.basic_possibility_tac")
   10.23 +apply basic_possibility
   10.24  apply (auto simp add: used_Cons symKeys_neq_imp_neq) 
   10.25  done
   10.26  
    11.1 --- a/src/HOL/SizeChange/sct.ML	Fri Mar 20 11:26:59 2009 +0100
    11.2 +++ b/src/HOL/SizeChange/sct.ML	Fri Mar 20 15:24:18 2009 +0100
    11.3 @@ -1,5 +1,4 @@
    11.4  (*  Title:      HOL/SizeChange/sct.ML
    11.5 -    ID:         $Id$
    11.6      Author:     Alexander Krauss, TU Muenchen
    11.7  
    11.8  Tactics for size change termination.
    11.9 @@ -183,8 +182,10 @@
   11.10  
   11.11  fun rand (_ $ t) = t
   11.12  
   11.13 -fun setup_probe_goal thy domT Dtab Mtab (i, j) =
   11.14 +fun setup_probe_goal ctxt domT Dtab Mtab (i, j) =
   11.15      let
   11.16 +      val css = local_clasimpset_of ctxt
   11.17 +      val thy = ProofContext.theory_of ctxt
   11.18        val RD1 = get_elem (Dtab i)
   11.19        val RD2 = get_elem (Dtab j)
   11.20        val Ms1 = get_elem (Mtab i)
   11.21 @@ -200,12 +201,12 @@
   11.22        val saved_state = HOLogic.mk_Trueprop (mk_stepP RD1 RD2 mvar1 mvar2 relvar)
   11.23                           |> cterm_of thy
   11.24                           |> Goal.init
   11.25 -                         |> CLASIMPSET auto_tac |> Seq.hd
   11.26 +                         |> auto_tac css |> Seq.hd
   11.27  
   11.28        val no_step = saved_state
   11.29                        |> forall_intr (cterm_of thy relvar)
   11.30                        |> forall_elim (cterm_of thy (Abs ("", HOLogic.natT, Abs ("", HOLogic.natT, HOLogic.false_const))))
   11.31 -                      |> CLASIMPSET auto_tac |> Seq.hd
   11.32 +                      |> auto_tac css |> Seq.hd
   11.33  
   11.34      in
   11.35        if Thm.no_prems no_step
   11.36 @@ -218,7 +219,7 @@
   11.37                  val with_m1 = saved_state
   11.38                                  |> forall_intr (cterm_of thy mvar1)
   11.39                                  |> forall_elim (cterm_of thy M1)
   11.40 -                                |> CLASIMPSET auto_tac |> Seq.hd
   11.41 +                                |> auto_tac css |> Seq.hd
   11.42  
   11.43                  fun set_m2 j =
   11.44                      let
   11.45 @@ -226,15 +227,15 @@
   11.46                        val with_m2 = with_m1
   11.47                                        |> forall_intr (cterm_of thy mvar2)
   11.48                                        |> forall_elim (cterm_of thy M2)
   11.49 -                                      |> CLASIMPSET auto_tac |> Seq.hd
   11.50 +                                      |> auto_tac css |> Seq.hd
   11.51  
   11.52                        val decr = forall_intr (cterm_of thy relvar)
   11.53                                     #> forall_elim (cterm_of thy @{const HOL.less(nat)})
   11.54 -                                   #> CLASIMPSET auto_tac #> Seq.hd
   11.55 +                                   #> auto_tac css #> Seq.hd
   11.56  
   11.57                        val decreq = forall_intr (cterm_of thy relvar)
   11.58                                       #> forall_elim (cterm_of thy @{const HOL.less_eq(nat)})
   11.59 -                                     #> CLASIMPSET auto_tac #> Seq.hd
   11.60 +                                     #> auto_tac css #> Seq.hd
   11.61  
   11.62                        val thm1 = decr with_m2
   11.63                      in
   11.64 @@ -266,17 +267,17 @@
   11.65  
   11.66  fun mk_edge m G n = HOLogic.mk_prod (m, HOLogic.mk_prod (G, n))
   11.67  
   11.68 -val in_graph_tac =
   11.69 +fun in_graph_tac ctxt =
   11.70      simp_tac (HOL_basic_ss addsimps has_edge_simps) 1
   11.71 -    THEN SIMPSET (fn x => simp_tac x 1) (* FIXME reduce simpset *)
   11.72 +    THEN (simp_tac (local_simpset_of ctxt) 1) (* FIXME reduce simpset *)
   11.73  
   11.74 -fun approx_tac (NoStep thm) = rtac disjI1 1 THEN rtac thm 1
   11.75 -  | approx_tac (Graph (G, thm)) =
   11.76 +fun approx_tac _ (NoStep thm) = rtac disjI1 1 THEN rtac thm 1
   11.77 +  | approx_tac ctxt (Graph (G, thm)) =
   11.78      rtac disjI2 1
   11.79      THEN rtac exI 1
   11.80      THEN rtac conjI 1
   11.81      THEN rtac thm 2
   11.82 -    THEN in_graph_tac
   11.83 +    THEN (in_graph_tac ctxt)
   11.84  
   11.85  fun all_less_tac [] = rtac all_less_zero 1
   11.86    | all_less_tac (t :: ts) = rtac all_less_Suc 1
   11.87 @@ -292,7 +293,7 @@
   11.88  
   11.89  fun mk_call_graph ctxt (st : thm) =
   11.90      let
   11.91 -      val thy = theory_of_thm st
   11.92 +      val thy = ProofContext.theory_of ctxt
   11.93        val _ $ _ $ RDlist $ _ = HOLogic.dest_Trueprop (hd (prems_of st))
   11.94  
   11.95        val RDs = HOLogic.dest_list RDlist
   11.96 @@ -316,7 +317,7 @@
   11.97        val pairs = matrix indices indices
   11.98        val parts = map_matrix (fn (n,m) =>
   11.99                                   (timeap_msg (string_of_int n ^ "," ^ string_of_int m)
  11.100 -                                             (setup_probe_goal thy domT Dtab Mtab) (n,m))) pairs
  11.101 +                                             (setup_probe_goal ctxt domT Dtab Mtab) (n,m))) pairs
  11.102  
  11.103  
  11.104        val s = fold_index (fn (i, cs) => fold_index (fn (j, Graph (G, _)) => prefix ("(" ^ string_of_int i ^ "," ^ string_of_int j ^ "): " ^
  11.105 @@ -333,8 +334,8 @@
  11.106        val sound_int_goal = HOLogic.mk_Trueprop (mk_sound_int ACG RDlist mfuns)
  11.107  
  11.108        val tac =
  11.109 -          (SIMPSET (unfold_tac [sound_int_def, len_simp]))
  11.110 -            THEN all_less_tac (map (all_less_tac o map approx_tac) parts)
  11.111 +          unfold_tac [sound_int_def, len_simp] (local_simpset_of ctxt)
  11.112 +            THEN all_less_tac (map (all_less_tac o map (approx_tac ctxt)) parts)
  11.113      in
  11.114        tac (instantiate' [] [SOME (cterm_of thy ACG), SOME (cterm_of thy mfuns)] st)
  11.115      end
    12.1 --- a/src/HOL/Tools/cnf_funcs.ML	Fri Mar 20 11:26:59 2009 +0100
    12.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Fri Mar 20 15:24:18 2009 +0100
    12.3 @@ -51,51 +51,46 @@
    12.4  structure cnf : CNF =
    12.5  struct
    12.6  
    12.7 -fun thm_by_auto (G : string) : thm =
    12.8 -	prove_goal (the_context ()) G (fn prems => [cut_facts_tac prems 1, CLASIMPSET auto_tac]);
    12.9 +val clause2raw_notE      = @{lemma "[| P; ~P |] ==> False" by auto};
   12.10 +val clause2raw_not_disj  = @{lemma "[| ~P; ~Q |] ==> ~(P | Q)" by auto};
   12.11 +val clause2raw_not_not   = @{lemma "P ==> ~~P" by auto};
   12.12  
   12.13 -(* Thm.thm *)
   12.14 -val clause2raw_notE      = thm_by_auto "[| P; ~P |] ==> False";
   12.15 -val clause2raw_not_disj  = thm_by_auto "[| ~P; ~Q |] ==> ~(P | Q)";
   12.16 -val clause2raw_not_not   = thm_by_auto "P ==> ~~P";
   12.17 +val iff_refl             = @{lemma "(P::bool) = P" by auto};
   12.18 +val iff_trans            = @{lemma "[| (P::bool) = Q; Q = R |] ==> P = R" by auto};
   12.19 +val conj_cong            = @{lemma "[| P = P'; Q = Q' |] ==> (P & Q) = (P' & Q')" by auto};
   12.20 +val disj_cong            = @{lemma "[| P = P'; Q = Q' |] ==> (P | Q) = (P' | Q')" by auto};
   12.21  
   12.22 -val iff_refl             = thm_by_auto "(P::bool) = P";
   12.23 -val iff_trans            = thm_by_auto "[| (P::bool) = Q; Q = R |] ==> P = R";
   12.24 -val conj_cong            = thm_by_auto "[| P = P'; Q = Q' |] ==> (P & Q) = (P' & Q')";
   12.25 -val disj_cong            = thm_by_auto "[| P = P'; Q = Q' |] ==> (P | Q) = (P' | Q')";
   12.26 -
   12.27 -val make_nnf_imp         = thm_by_auto "[| (~P) = P'; Q = Q' |] ==> (P --> Q) = (P' | Q')";
   12.28 -val make_nnf_iff         = thm_by_auto "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' | NQ) & (NP | Q'))";
   12.29 -val make_nnf_not_false   = thm_by_auto "(~False) = True";
   12.30 -val make_nnf_not_true    = thm_by_auto "(~True) = False";
   12.31 -val make_nnf_not_conj    = thm_by_auto "[| (~P) = P'; (~Q) = Q' |] ==> (~(P & Q)) = (P' | Q')";
   12.32 -val make_nnf_not_disj    = thm_by_auto "[| (~P) = P'; (~Q) = Q' |] ==> (~(P | Q)) = (P' & Q')";
   12.33 -val make_nnf_not_imp     = thm_by_auto "[| P = P'; (~Q) = Q' |] ==> (~(P --> Q)) = (P' & Q')";
   12.34 -val make_nnf_not_iff     = thm_by_auto "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' | Q') & (NP | NQ))";
   12.35 -val make_nnf_not_not     = thm_by_auto "P = P' ==> (~~P) = P'";
   12.36 +val make_nnf_imp         = @{lemma "[| (~P) = P'; Q = Q' |] ==> (P --> Q) = (P' | Q')" by auto};
   12.37 +val make_nnf_iff         = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' | NQ) & (NP | Q'))" by auto};
   12.38 +val make_nnf_not_false   = @{lemma "(~False) = True" by auto};
   12.39 +val make_nnf_not_true    = @{lemma "(~True) = False" by auto};
   12.40 +val make_nnf_not_conj    = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P & Q)) = (P' | Q')" by auto};
   12.41 +val make_nnf_not_disj    = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P | Q)) = (P' & Q')" by auto};
   12.42 +val make_nnf_not_imp     = @{lemma "[| P = P'; (~Q) = Q' |] ==> (~(P --> Q)) = (P' & Q')" by auto};
   12.43 +val make_nnf_not_iff     = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' | Q') & (NP | NQ))" by auto};
   12.44 +val make_nnf_not_not     = @{lemma "P = P' ==> (~~P) = P'" by auto};
   12.45  
   12.46 -val simp_TF_conj_True_l  = thm_by_auto "[| P = True; Q = Q' |] ==> (P & Q) = Q'";
   12.47 -val simp_TF_conj_True_r  = thm_by_auto "[| P = P'; Q = True |] ==> (P & Q) = P'";
   12.48 -val simp_TF_conj_False_l = thm_by_auto "P = False ==> (P & Q) = False";
   12.49 -val simp_TF_conj_False_r = thm_by_auto "Q = False ==> (P & Q) = False";
   12.50 -val simp_TF_disj_True_l  = thm_by_auto "P = True ==> (P | Q) = True";
   12.51 -val simp_TF_disj_True_r  = thm_by_auto "Q = True ==> (P | Q) = True";
   12.52 -val simp_TF_disj_False_l = thm_by_auto "[| P = False; Q = Q' |] ==> (P | Q) = Q'";
   12.53 -val simp_TF_disj_False_r = thm_by_auto "[| P = P'; Q = False |] ==> (P | Q) = P'";
   12.54 +val simp_TF_conj_True_l  = @{lemma "[| P = True; Q = Q' |] ==> (P & Q) = Q'" by auto};
   12.55 +val simp_TF_conj_True_r  = @{lemma "[| P = P'; Q = True |] ==> (P & Q) = P'" by auto};
   12.56 +val simp_TF_conj_False_l = @{lemma "P = False ==> (P & Q) = False" by auto};
   12.57 +val simp_TF_conj_False_r = @{lemma "Q = False ==> (P & Q) = False" by auto};
   12.58 +val simp_TF_disj_True_l  = @{lemma "P = True ==> (P | Q) = True" by auto};
   12.59 +val simp_TF_disj_True_r  = @{lemma "Q = True ==> (P | Q) = True" by auto};
   12.60 +val simp_TF_disj_False_l = @{lemma "[| P = False; Q = Q' |] ==> (P | Q) = Q'" by auto};
   12.61 +val simp_TF_disj_False_r = @{lemma "[| P = P'; Q = False |] ==> (P | Q) = P'" by auto};
   12.62  
   12.63 -val make_cnf_disj_conj_l = thm_by_auto "[| (P | R) = PR; (Q | R) = QR |] ==> ((P & Q) | R) = (PR & QR)";
   12.64 -val make_cnf_disj_conj_r = thm_by_auto "[| (P | Q) = PQ; (P | R) = PR |] ==> (P | (Q & R)) = (PQ & PR)";
   12.65 +val make_cnf_disj_conj_l = @{lemma "[| (P | R) = PR; (Q | R) = QR |] ==> ((P & Q) | R) = (PR & QR)" by auto};
   12.66 +val make_cnf_disj_conj_r = @{lemma "[| (P | Q) = PQ; (P | R) = PR |] ==> (P | (Q & R)) = (PQ & PR)" by auto};
   12.67  
   12.68 -val make_cnfx_disj_ex_l = thm_by_auto "((EX (x::bool). P x) | Q) = (EX x. P x | Q)";
   12.69 -val make_cnfx_disj_ex_r = thm_by_auto "(P | (EX (x::bool). Q x)) = (EX x. P | Q x)";
   12.70 -val make_cnfx_newlit    = thm_by_auto "(P | Q) = (EX x. (P | x) & (Q | ~x))";
   12.71 -val make_cnfx_ex_cong   = thm_by_auto "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)";
   12.72 +val make_cnfx_disj_ex_l  = @{lemma "((EX (x::bool). P x) | Q) = (EX x. P x | Q)" by auto};
   12.73 +val make_cnfx_disj_ex_r  = @{lemma "(P | (EX (x::bool). Q x)) = (EX x. P | Q x)" by auto};
   12.74 +val make_cnfx_newlit     = @{lemma "(P | Q) = (EX x. (P | x) & (Q | ~x))" by auto};
   12.75 +val make_cnfx_ex_cong    = @{lemma "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)" by auto};
   12.76  
   12.77 -val weakening_thm        = thm_by_auto "[| P; Q |] ==> Q";
   12.78 +val weakening_thm        = @{lemma "[| P; Q |] ==> Q" by auto};
   12.79  
   12.80 -val cnftac_eq_imp        = thm_by_auto "[| P = Q; P |] ==> Q";
   12.81 +val cnftac_eq_imp        = @{lemma "[| P = Q; P |] ==> Q" by auto};
   12.82  
   12.83 -(* Term.term -> bool *)
   12.84  fun is_atom (Const ("False", _))                                           = false
   12.85    | is_atom (Const ("True", _))                                            = false
   12.86    | is_atom (Const ("op &", _) $ _ $ _)                                    = false
   12.87 @@ -105,11 +100,9 @@
   12.88    | is_atom (Const ("Not", _) $ _)                                         = false
   12.89    | is_atom _                                                              = true;
   12.90  
   12.91 -(* Term.term -> bool *)
   12.92  fun is_literal (Const ("Not", _) $ x) = is_atom x
   12.93    | is_literal x                      = is_atom x;
   12.94  
   12.95 -(* Term.term -> bool *)
   12.96  fun is_clause (Const ("op |", _) $ x $ y) = is_clause x andalso is_clause y
   12.97    | is_clause x                           = is_literal x;
   12.98  
    13.1 --- a/src/HOL/Tools/function_package/fundef_core.ML	Fri Mar 20 11:26:59 2009 +0100
    13.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML	Fri Mar 20 15:24:18 2009 +0100
    13.3 @@ -691,8 +691,9 @@
    13.4  
    13.5  
    13.6  (* FIXME: This should probably use fixed goals, to be more reliable and faster *)
    13.7 -fun mk_domain_intro thy (Globals {domT, ...}) R R_cases clause =
    13.8 +fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
    13.9      let
   13.10 +      val thy = ProofContext.theory_of ctxt
   13.11        val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
   13.12                        qglr = (oqs, _, _, _), ...} = clause
   13.13        val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
   13.14 @@ -702,7 +703,7 @@
   13.15        Goal.init goal
   13.16        |> (SINGLE (resolve_tac [accI] 1)) |> the
   13.17        |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1))  |> the
   13.18 -      |> (SINGLE (CLASIMPSET auto_tac)) |> the
   13.19 +      |> (SINGLE (auto_tac (local_clasimpset_of ctxt))) |> the
   13.20        |> Goal.conclude
   13.21        |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   13.22      end
   13.23 @@ -831,7 +832,7 @@
   13.24                           ((rtac (G_induct OF [a]))
   13.25                              THEN_ALL_NEW (rtac accI)
   13.26                              THEN_ALL_NEW (etac R_cases)
   13.27 -                            THEN_ALL_NEW (SIMPSET' asm_full_simp_tac)) 1)
   13.28 +                            THEN_ALL_NEW (asm_full_simp_tac (local_simpset_of octxt))) 1)
   13.29  
   13.30        val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value)
   13.31  
   13.32 @@ -849,9 +850,9 @@
   13.33                         (fn _ =>
   13.34                             rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
   13.35                                  THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
   13.36 -                                THEN (SIMPSET' simp_default_tac 1)
   13.37 +                                THEN (simp_default_tac (local_simpset_of ctxt) 1)
   13.38                                  THEN (etac not_acc_down 1)
   13.39 -                                THEN ((etac R_cases) THEN_ALL_NEW (SIMPSET' simp_default_tac)) 1)
   13.40 +                                THEN ((etac R_cases) THEN_ALL_NEW (simp_default_tac (local_simpset_of ctxt))) 1)
   13.41                |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   13.42            end
   13.43      in
   13.44 @@ -935,7 +936,7 @@
   13.45              val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses
   13.46  
   13.47              val dom_intros = if domintros
   13.48 -                             then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro newthy globals R R_elim)) xclauses)
   13.49 +                             then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro lthy globals R R_elim)) xclauses)
   13.50                               else NONE
   13.51              val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
   13.52  
    14.1 --- a/src/HOL/Tools/function_package/mutual.ML	Fri Mar 20 11:26:59 2009 +0100
    14.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Fri Mar 20 15:24:18 2009 +0100
    14.3 @@ -1,5 +1,4 @@
    14.4  (*  Title:      HOL/Tools/function_package/mutual.ML
    14.5 -    ID:         $Id$
    14.6      Author:     Alexander Krauss, TU Muenchen
    14.7  
    14.8  A package for general recursive function definitions.
    14.9 @@ -207,7 +206,7 @@
   14.10                   (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
   14.11                   (fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs)
   14.12                            THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
   14.13 -                          THEN SIMPSET' (fn ss => simp_tac (ss addsimps SumTree.proj_in_rules)) 1)
   14.14 +                          THEN (simp_tac (local_simpset_of ctxt addsimps SumTree.proj_in_rules)) 1)
   14.15          |> restore_cond 
   14.16          |> export
   14.17      end
    15.1 --- a/src/HOL/Tools/function_package/scnp_reconstruct.ML	Fri Mar 20 11:26:59 2009 +0100
    15.2 +++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML	Fri Mar 20 15:24:18 2009 +0100
    15.3 @@ -291,7 +291,7 @@
    15.4           THEN (rtac @{thm rp_inv_image_rp} 1)
    15.5           THEN (rtac (order_rpair ms_rp label) 1)
    15.6           THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
    15.7 -         THEN unfold_tac @{thms rp_inv_image_def} (simpset_of thy)
    15.8 +         THEN unfold_tac @{thms rp_inv_image_def} (local_simpset_of ctxt)
    15.9           THEN LocalDefs.unfold_tac ctxt
   15.10             (@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
   15.11           THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
   15.12 @@ -395,7 +395,7 @@
   15.13  
   15.14  fun gen_sizechange_tac orders autom_tac ctxt err_cont =
   15.15    TRY (FundefCommon.apply_termination_rule ctxt 1)
   15.16 -  THEN TRY Termination.wf_union_tac
   15.17 +  THEN TRY (Termination.wf_union_tac ctxt)
   15.18    THEN
   15.19     (rtac @{thm wf_empty} 1
   15.20      ORELSE gen_decomp_scnp_tac orders autom_tac ctxt err_cont 1)
    16.1 --- a/src/HOL/Tools/function_package/termination.ML	Fri Mar 20 11:26:59 2009 +0100
    16.2 +++ b/src/HOL/Tools/function_package/termination.ML	Fri Mar 20 15:24:18 2009 +0100
    16.3 @@ -40,7 +40,7 @@
    16.4  
    16.5    val REPEAT : ttac -> ttac
    16.6  
    16.7 -  val wf_union_tac : tactic
    16.8 +  val wf_union_tac : Proof.context -> tactic
    16.9  end
   16.10  
   16.11  
   16.12 @@ -276,9 +276,9 @@
   16.13  
   16.14  in
   16.15  
   16.16 -fun wf_union_tac st =
   16.17 +fun wf_union_tac ctxt st =
   16.18      let
   16.19 -      val thy = theory_of_thm st
   16.20 +      val thy = ProofContext.theory_of ctxt
   16.21        val cert = cterm_of (theory_of_thm st)
   16.22        val ((trueprop $ (wf $ rel)) :: ineqs) = prems_of st
   16.23  
   16.24 @@ -303,7 +303,7 @@
   16.25            THEN' ((rtac @{thm refl})                       (* unification instantiates all Vars *)
   16.26                   ORELSE' ((rtac @{thm conjI})
   16.27                            THEN' (rtac @{thm refl})
   16.28 -                          THEN' (CLASET' blast_tac)))     (* Solve rest of context... not very elegant *)
   16.29 +                          THEN' (blast_tac (local_claset_of ctxt))))  (* Solve rest of context... not very elegant *)
   16.30            ) i
   16.31      in
   16.32        ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
    17.1 --- a/src/HOL/Tools/meson.ML	Fri Mar 20 11:26:59 2009 +0100
    17.2 +++ b/src/HOL/Tools/meson.ML	Fri Mar 20 15:24:18 2009 +0100
    17.3 @@ -25,7 +25,7 @@
    17.4    val skolemize_prems_tac: thm list -> int -> tactic
    17.5    val MESON: (thm list -> thm list) -> (thm list -> tactic) -> int -> tactic
    17.6    val best_meson_tac: (thm -> int) -> int -> tactic
    17.7 -  val safe_best_meson_tac: int -> tactic
    17.8 +  val safe_best_meson_tac: claset -> int -> tactic
    17.9    val depth_meson_tac: int -> tactic
   17.10    val prolog_step_tac': thm list -> int -> tactic
   17.11    val iter_deepen_prolog_tac: thm list -> tactic
   17.12 @@ -33,7 +33,7 @@
   17.13    val make_meta_clause: thm -> thm
   17.14    val make_meta_clauses: thm list -> thm list
   17.15    val meson_claset_tac: thm list -> claset -> int -> tactic
   17.16 -  val meson_tac: int -> tactic
   17.17 +  val meson_tac: claset -> int -> tactic
   17.18    val negate_head: thm -> thm
   17.19    val select_literal: int -> thm -> thm
   17.20    val skolemize_tac: int -> tactic
   17.21 @@ -589,8 +589,8 @@
   17.22                           (prolog_step_tac (make_horns cls) 1));
   17.23  
   17.24  (*First, breaks the goal into independent units*)
   17.25 -val safe_best_meson_tac =
   17.26 -     SELECT_GOAL (TRY (CLASET safe_tac) THEN
   17.27 +fun safe_best_meson_tac cs =
   17.28 +     SELECT_GOAL (TRY (safe_tac cs) THEN
   17.29                    TRYALL (best_meson_tac size_of_subgoals));
   17.30  
   17.31  (** Depth-first search version **)
   17.32 @@ -634,7 +634,7 @@
   17.33  fun meson_claset_tac ths cs =
   17.34    SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
   17.35  
   17.36 -val meson_tac = CLASET' (meson_claset_tac []);
   17.37 +val meson_tac = meson_claset_tac [];
   17.38  
   17.39  
   17.40  (**** Code to support ordinary resolution, rather than Model Elimination ****)
    18.1 --- a/src/HOL/Word/WordArith.thy	Fri Mar 20 11:26:59 2009 +0100
    18.2 +++ b/src/HOL/Word/WordArith.thy	Fri Mar 20 15:24:18 2009 +0100
    18.3 @@ -511,10 +511,13 @@
    18.4       addcongs @{thms power_False_cong}
    18.5  
    18.6  fun uint_arith_tacs ctxt = 
    18.7 -  let fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty  
    18.8 +  let
    18.9 +    fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty;
   18.10 +    val cs = local_claset_of ctxt;
   18.11 +    val ss = local_simpset_of ctxt;
   18.12    in 
   18.13 -    [ CLASET' clarify_tac 1,
   18.14 -      SIMPSET' (full_simp_tac o uint_arith_ss_of) 1,
   18.15 +    [ clarify_tac cs 1,
   18.16 +      full_simp_tac (uint_arith_ss_of ss) 1,
   18.17        ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms uint_splits} 
   18.18                                        addcongs @{thms power_False_cong})),
   18.19        rewrite_goals_tac @{thms word_size}, 
   18.20 @@ -1069,10 +1072,13 @@
   18.21       addcongs @{thms power_False_cong}
   18.22  
   18.23  fun unat_arith_tacs ctxt =   
   18.24 -  let fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty  
   18.25 +  let
   18.26 +    fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty;
   18.27 +    val cs = local_claset_of ctxt;
   18.28 +    val ss = local_simpset_of ctxt;
   18.29    in 
   18.30 -    [ CLASET' clarify_tac 1,
   18.31 -      SIMPSET' (full_simp_tac o unat_arith_ss_of) 1,
   18.32 +    [ clarify_tac cs 1,
   18.33 +      full_simp_tac (unat_arith_ss_of ss) 1,
   18.34        ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms unat_splits} 
   18.35                                         addcongs @{thms power_False_cong})),
   18.36        rewrite_goals_tac @{thms word_size}, 
    19.1 --- a/src/HOL/ex/Classical.thy	Fri Mar 20 11:26:59 2009 +0100
    19.2 +++ b/src/HOL/ex/Classical.thy	Fri Mar 20 15:24:18 2009 +0100
    19.3 @@ -1,5 +1,4 @@
    19.4  (*  Title:      HOL/ex/Classical
    19.5 -    ID:         $Id$
    19.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    19.7      Copyright   1994  University of Cambridge
    19.8  *)
    19.9 @@ -430,7 +429,7 @@
   19.10  lemma "(\<forall>x y z. R(x,y) & R(y,z) --> R(x,z)) &
   19.11         (\<forall>x. \<exists>y. R(x,y)) -->
   19.12         ~ (\<forall>x. P x = (\<forall>y. R(x,y) --> ~ P y))"
   19.13 -by (tactic{*Meson.safe_best_meson_tac 1*})
   19.14 +by (tactic{*Meson.safe_best_meson_tac @{claset} 1*})
   19.15      --{*In contrast, @{text meson} is SLOW: 7.6s on griffon*}
   19.16  
   19.17  
   19.18 @@ -724,7 +723,7 @@
   19.19         (\<forall>x y. bird x & snail y \<longrightarrow> ~eats x y) &
   19.20         (\<forall>x. (caterpillar x \<or> snail x) \<longrightarrow> (\<exists>y. plant y & eats x y))
   19.21         \<longrightarrow> (\<exists>x y. animal x & animal y & (\<exists>z. grain z & eats y z & eats x y))"
   19.22 -by (tactic{*Meson.safe_best_meson_tac 1*})
   19.23 +by (tactic{*Meson.safe_best_meson_tac @{claset} 1*})
   19.24      --{*Nearly twice as fast as @{text meson},
   19.25          which performs iterative deepening rather than best-first search*}
   19.26  
    20.1 --- a/src/HOLCF/IOA/ex/TrivEx.thy	Fri Mar 20 11:26:59 2009 +0100
    20.2 +++ b/src/HOLCF/IOA/ex/TrivEx.thy	Fri Mar 20 15:24:18 2009 +0100
    20.3 @@ -1,5 +1,4 @@
    20.4  (*  Title:      HOLCF/IOA/TrivEx.thy
    20.5 -    ID:         $Id$
    20.6      Author:     Olaf Müller
    20.7  *)
    20.8  
    20.9 @@ -66,7 +65,7 @@
   20.10  apply (rule AbsRuleT1)
   20.11  apply (rule h_abs_is_abstraction)
   20.12  apply (rule MC_result)
   20.13 -apply (tactic "abstraction_tac 1")
   20.14 +apply abstraction
   20.15  apply (simp add: h_abs_def)
   20.16  done
   20.17  
    21.1 --- a/src/HOLCF/IOA/ex/TrivEx2.thy	Fri Mar 20 11:26:59 2009 +0100
    21.2 +++ b/src/HOLCF/IOA/ex/TrivEx2.thy	Fri Mar 20 15:24:18 2009 +0100
    21.3 @@ -1,5 +1,4 @@
    21.4  (*  Title:      HOLCF/IOA/TrivEx.thy
    21.5 -    ID:         $Id$
    21.6      Author:     Olaf Müller
    21.7  *)
    21.8  
    21.9 @@ -85,7 +84,7 @@
   21.10  txt {* is_abstraction *}
   21.11  apply (rule h_abs_is_abstraction)
   21.12  txt {* temp_weakening *}
   21.13 -apply (tactic "abstraction_tac 1")
   21.14 +apply abstraction
   21.15  apply (erule Enabled_implication)
   21.16  done
   21.17  
   21.18 @@ -96,7 +95,7 @@
   21.19  apply (rule AbsRuleT2)
   21.20  apply (rule h_abs_is_liveabstraction)
   21.21  apply (rule MC_result)
   21.22 -apply (tactic "abstraction_tac 1")
   21.23 +apply abstraction
   21.24  apply (simp add: h_abs_def)
   21.25  done
   21.26  
    22.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Fri Mar 20 11:26:59 2009 +0100
    22.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Fri Mar 20 15:24:18 2009 +0100
    22.3 @@ -1,5 +1,4 @@
    22.4  (*  Title:      HOLCF/IOA/meta_theory/Abstraction.thy
    22.5 -    ID:         $Id$
    22.6      Author:     Olaf Müller
    22.7  *)
    22.8  
    22.9 @@ -605,12 +604,15 @@
   22.10    strength_Diamond strength_Leadsto weak_WF weak_SF
   22.11  
   22.12  ML {*
   22.13 -fun abstraction_tac i =
   22.14 -    SELECT_GOAL (CLASIMPSET (fn (cs, ss) =>
   22.15 -      auto_tac (cs addSIs @{thms weak_strength_lemmas},
   22.16 -        ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}]))) i
   22.17 +fun abstraction_tac ctxt =
   22.18 +  let val (cs, ss) = local_clasimpset_of ctxt in
   22.19 +    SELECT_GOAL (auto_tac (cs addSIs @{thms weak_strength_lemmas},
   22.20 +        ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}]))
   22.21 +  end
   22.22  *}
   22.23  
   22.24 +method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} ""
   22.25 +
   22.26  use "ioa_package.ML"
   22.27  
   22.28  end
    23.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Fri Mar 20 11:26:59 2009 +0100
    23.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Fri Mar 20 15:24:18 2009 +0100
    23.3 @@ -1,5 +1,4 @@
    23.4  (*  Title:      HOLCF/IOA/meta_theory/Sequence.thy
    23.5 -    ID:         $Id$
    23.6      Author:     Olaf Müller
    23.7  
    23.8  Sequences over flat domains with lifted elements.
    23.9 @@ -340,7 +339,7 @@
   23.10  lemma Seq_induct:
   23.11  "!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x"
   23.12  apply (erule (2) seq.ind)
   23.13 -apply (tactic {* def_tac 1 *})
   23.14 +apply defined
   23.15  apply (simp add: Consq_def)
   23.16  done
   23.17  
   23.18 @@ -348,14 +347,14 @@
   23.19  "!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |]
   23.20                  ==> seq_finite x --> P x"
   23.21  apply (erule (1) seq_finite_ind)
   23.22 -apply (tactic {* def_tac 1 *})
   23.23 +apply defined
   23.24  apply (simp add: Consq_def)
   23.25  done
   23.26  
   23.27  lemma Seq_Finite_ind:
   23.28  "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x"
   23.29  apply (erule (1) Finite.induct)
   23.30 -apply (tactic {* def_tac 1 *})
   23.31 +apply defined
   23.32  apply (simp add: Consq_def)
   23.33  done
   23.34  
    24.1 --- a/src/HOLCF/IOA/meta_theory/Traces.thy	Fri Mar 20 11:26:59 2009 +0100
    24.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Fri Mar 20 15:24:18 2009 +0100
    24.3 @@ -1,5 +1,4 @@
    24.4  (*  Title:      HOLCF/IOA/meta_theory/Traces.thy
    24.5 -    ID:         $Id$
    24.6      Author:     Olaf Müller
    24.7  *)
    24.8  
    24.9 @@ -327,7 +326,7 @@
   24.10  apply (simp (no_asm_simp))
   24.11  apply (drule Finite_Last1 [THEN mp])
   24.12  apply assumption
   24.13 -apply (tactic "def_tac 1")
   24.14 +apply defined
   24.15  done
   24.16  
   24.17  declare laststate_UU [simp] laststate_nil [simp] laststate_cons [simp]
    25.1 --- a/src/HOLCF/Lift.thy	Fri Mar 20 11:26:59 2009 +0100
    25.2 +++ b/src/HOLCF/Lift.thy	Fri Mar 20 15:24:18 2009 +0100
    25.3 @@ -56,15 +56,13 @@
    25.4    by (cases x) simp_all
    25.5  
    25.6  text {*
    25.7 -  For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text
    25.8 +  For @{term "x ~= UU"} in assumptions @{text defined} replaces @{text
    25.9    x} by @{text "Def a"} in conclusion. *}
   25.10  
   25.11 -ML {*
   25.12 -  local val lift_definedE = thm "lift_definedE"
   25.13 -  in val def_tac = SIMPSET' (fn ss =>
   25.14 -    etac lift_definedE THEN' asm_simp_tac ss)
   25.15 -  end;
   25.16 -*}
   25.17 +method_setup defined = {*
   25.18 +  Scan.succeed (fn ctxt => SIMPLE_METHOD'
   25.19 +    (etac @{thm lift_definedE} THEN' asm_simp_tac (local_simpset_of ctxt)))
   25.20 +*} ""
   25.21  
   25.22  lemma DefE: "Def x = \<bottom> \<Longrightarrow> R"
   25.23    by simp
    26.1 --- a/src/Sequents/LK.thy	Fri Mar 20 11:26:59 2009 +0100
    26.2 +++ b/src/Sequents/LK.thy	Fri Mar 20 15:24:18 2009 +0100
    26.3 @@ -226,9 +226,9 @@
    26.4  
    26.5  lemma split_if: "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
    26.6    apply (rule_tac P = Q in cut)
    26.7 -   apply (tactic {* simp_tac (simpset () addsimps @{thms if_P}) 2 *})
    26.8 +   apply (tactic {* simp_tac (@{simpset} addsimps @{thms if_P}) 2 *})
    26.9    apply (rule_tac P = "~Q" in cut)
   26.10 -   apply (tactic {* simp_tac (simpset() addsimps @{thms if_not_P}) 2 *})
   26.11 +   apply (tactic {* simp_tac (@{simpset} addsimps @{thms if_not_P}) 2 *})
   26.12    apply (tactic {* fast_tac LK_pack 1 *})
   26.13    done
   26.14  
    27.1 --- a/src/ZF/int_arith.ML	Fri Mar 20 11:26:59 2009 +0100
    27.2 +++ b/src/ZF/int_arith.ML	Fri Mar 20 15:24:18 2009 +0100
    27.3 @@ -145,7 +145,7 @@
    27.4    val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
    27.5    fun numeral_simp_tac ss =
    27.6      ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
    27.7 -    THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_context ss simpset)))
    27.8 +    THEN ALLGOALS (asm_simp_tac (local_simpset_of (Simplifier.the_context ss)))
    27.9    val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
   27.10    end;
   27.11