src/HOLCF/IOA/meta_theory/Sequence.ML

 (* ---------------------------------------------------------------- *)
 (*                               Map                                *)
 (* ---------------------------------------------------------------- *)
 
 goal thy "Map f`UU =UU";
-by (simp_tac (!simpset addsimps [Map_def]) 1);
+by (simp_tac (simpset() addsimps [Map_def]) 1);
 qed"Map_UU";
 
 goal thy "Map f`nil =nil";
-by (simp_tac (!simpset addsimps [Map_def]) 1);
+by (simp_tac (simpset() addsimps [Map_def]) 1);
 qed"Map_nil";
 
 goal thy "Map f`(x>>xs)=(f x) >> Map f`xs";
-by (simp_tac (!simpset addsimps [Map_def, Cons_def,flift2_def]) 1);
+by (simp_tac (simpset() addsimps [Map_def, Cons_def,flift2_def]) 1);
 qed"Map_cons";
 
 (* ---------------------------------------------------------------- *)
 (*                               Filter                             *)
 (* ---------------------------------------------------------------- *)
 
 goal thy "Filter P`UU =UU";
-by (simp_tac (!simpset addsimps [Filter_def]) 1);
+by (simp_tac (simpset() addsimps [Filter_def]) 1);
 qed"Filter_UU";
 
 goal thy "Filter P`nil =nil";
-by (simp_tac (!simpset addsimps [Filter_def]) 1);
+by (simp_tac (simpset() addsimps [Filter_def]) 1);
 qed"Filter_nil";
 
 goal thy "Filter P`(x>>xs)= (if P x then x>>(Filter P`xs) else Filter P`xs)"; 
-by (simp_tac (!simpset addsimps [Filter_def, Cons_def,flift2_def,If_and_if]) 1);
+by (simp_tac (simpset() addsimps [Filter_def, Cons_def,flift2_def,If_and_if]) 1);
 qed"Filter_cons";
 
 (* ---------------------------------------------------------------- *)
 (*                               Forall                             *)
 (* ---------------------------------------------------------------- *)
 
 goal thy "Forall P UU";
-by (simp_tac (!simpset addsimps [Forall_def,sforall_def]) 1);
+by (simp_tac (simpset() addsimps [Forall_def,sforall_def]) 1);
 qed"Forall_UU";
 
 goal thy "Forall P nil";
-by (simp_tac (!simpset addsimps [Forall_def,sforall_def]) 1);
+by (simp_tac (simpset() addsimps [Forall_def,sforall_def]) 1);
 qed"Forall_nil";
 
 goal thy "Forall P (x>>xs)= (P x & Forall P xs)";
-by (simp_tac (!simpset addsimps [Forall_def, sforall_def,
+by (simp_tac (simpset() addsimps [Forall_def, sforall_def,
                                  Cons_def,flift2_def]) 1);
 qed"Forall_cons";
 
 (* ---------------------------------------------------------------- *)
 (*                               Conc                               *)
 (* ---------------------------------------------------------------- *)
 
 
 goal thy "(x>>xs) @@ y = x>>(xs @@y)"; 
-by (simp_tac (!simpset addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Cons_def]) 1);
 qed"Conc_cons";
 
 (* ---------------------------------------------------------------- *)
 (*                               Takewhile                          *)
 (* ---------------------------------------------------------------- *)
 
 goal thy "Takewhile P`UU =UU";
-by (simp_tac (!simpset addsimps [Takewhile_def]) 1);
+by (simp_tac (simpset() addsimps [Takewhile_def]) 1);
 qed"Takewhile_UU";
 
 goal thy "Takewhile P`nil =nil";
-by (simp_tac (!simpset addsimps [Takewhile_def]) 1);
+by (simp_tac (simpset() addsimps [Takewhile_def]) 1);
 qed"Takewhile_nil";
 
 goal thy "Takewhile P`(x>>xs)= (if P x then x>>(Takewhile P`xs) else nil)"; 
-by (simp_tac (!simpset addsimps [Takewhile_def, Cons_def,flift2_def,If_and_if]) 1);
+by (simp_tac (simpset() addsimps [Takewhile_def, Cons_def,flift2_def,If_and_if]) 1);
 qed"Takewhile_cons";
 
 (* ---------------------------------------------------------------- *)
 (*                               Dropwhile                          *)
 (* ---------------------------------------------------------------- *)
 
 goal thy "Dropwhile P`UU =UU";
-by (simp_tac (!simpset addsimps [Dropwhile_def]) 1);
+by (simp_tac (simpset() addsimps [Dropwhile_def]) 1);
 qed"Dropwhile_UU";
 
 goal thy "Dropwhile P`nil =nil";
-by (simp_tac (!simpset addsimps [Dropwhile_def]) 1);
+by (simp_tac (simpset() addsimps [Dropwhile_def]) 1);
 qed"Dropwhile_nil";
 
 goal thy "Dropwhile P`(x>>xs)= (if P x then Dropwhile P`xs else x>>xs)"; 
-by (simp_tac (!simpset addsimps [Dropwhile_def, Cons_def,flift2_def,If_and_if]) 1);
+by (simp_tac (simpset() addsimps [Dropwhile_def, Cons_def,flift2_def,If_and_if]) 1);
 qed"Dropwhile_cons";
 
 (* ---------------------------------------------------------------- *)
 (*                               Last                               *)
 (* ---------------------------------------------------------------- *)
 
 
 goal thy "Last`UU =UU";
-by (simp_tac (!simpset addsimps [Last_def]) 1);
+by (simp_tac (simpset() addsimps [Last_def]) 1);
 qed"Last_UU";
 
 goal thy "Last`nil =UU";
-by (simp_tac (!simpset addsimps [Last_def]) 1);
+by (simp_tac (simpset() addsimps [Last_def]) 1);
 qed"Last_nil";
 
 goal thy "Last`(x>>xs)= (if xs=nil then Def x else Last`xs)"; 
-by (simp_tac (!simpset addsimps [Last_def, Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Last_def, Cons_def]) 1);
 by (res_inst_tac [("x","xs")] seq.casedist 1);
-by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
 by (REPEAT (Asm_simp_tac 1));
 qed"Last_cons";
 
 
 (* ---------------------------------------------------------------- *)
 (*                               Flat                               *)
 (* ---------------------------------------------------------------- *)
 
 goal thy "Flat`UU =UU";
-by (simp_tac (!simpset addsimps [Flat_def]) 1);
+by (simp_tac (simpset() addsimps [Flat_def]) 1);
 qed"Flat_UU";
 
 goal thy "Flat`nil =nil";
-by (simp_tac (!simpset addsimps [Flat_def]) 1);
+by (simp_tac (simpset() addsimps [Flat_def]) 1);
 qed"Flat_nil";
 
 goal thy "Flat`(x##xs)= x @@ (Flat`xs)"; 
-by (simp_tac (!simpset addsimps [Flat_def, Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Flat_def, Cons_def]) 1);
 qed"Flat_cons";
 
 
 (* ---------------------------------------------------------------- *)
 (*                               Zip                                *)

 by (Simp_tac 1);
 qed"Zip_nil";
 
 goal thy "Zip`(x>>xs)`nil= UU"; 
 by (stac Zip_unfold 1);
-by (simp_tac (!simpset addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Cons_def]) 1);
 qed"Zip_cons_nil";
 
 goal thy "Zip`(x>>xs)`(y>>ys)= (x,y) >> Zip`xs`ys"; 
 by (rtac trans 1);
 by (stac Zip_unfold 1);
 by (Simp_tac 1);
 (* FIX: Why Simp_tac 2 times. Does continuity in simpflication make job sometimes not 
   completely ready ? *)
-by (simp_tac (!simpset addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Cons_def]) 1);
 qed"Zip_cons";
 
 
 Delsimps [sfilter_UU,sfilter_nil,sfilter_cons,
           smap_UU,smap_nil,smap_cons,

 
 
 section "Cons";
 
 goal thy "a>>s = (Def a)##s";
-by (simp_tac (!simpset addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Cons_def]) 1);
 qed"Cons_def2";
 
 goal thy "x = UU | x = nil | (? a s. x = a >> s)";
-by (simp_tac (!simpset addsimps [Cons_def2]) 1);
+by (simp_tac (simpset() addsimps [Cons_def2]) 1);
 by (cut_facts_tac [seq.exhaust] 1);
 by (fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1]) 1);
 qed"Seq_exhaust";
 
 

 
 goal thy "~(a>>x) << UU";
 by (rtac notI 1);
 by (dtac antisym_less 1);
 by (Simp_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_not_UU]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_not_UU]) 1);
 qed"Cons_not_less_UU";
 
 goal thy "~a>>s << nil";
 by (stac Cons_def2 1);
 by (resolve_tac seq.rews 1);

 by (stac Cons_def2 1);
 by (resolve_tac seq.rews 1);
 qed"Cons_not_nil";
 
 goal thy "nil ~= a>>s";
-by (simp_tac (!simpset addsimps [Cons_def2]) 1);
+by (simp_tac (simpset() addsimps [Cons_def2]) 1);
 qed"Cons_not_nil2";
 
 goal thy "(a>>s = b>>t) = (a = b & s = t)";
 by (simp_tac (HOL_ss addsimps [Cons_def2]) 1);
 by (stac (hd lift.inject RS sym) 1);

 by (rtac scons_inject_eq 1);
 by (REPEAT(rtac Def_not_UU 1));
 qed"Cons_inject_eq";
 
 goal thy "(a>>s<<b>>t) = (a = b & s<<t)";
-by (simp_tac (!simpset addsimps [Cons_def2]) 1);
+by (simp_tac (simpset() addsimps [Cons_def2]) 1);
 by (stac (Def_inject_less_eq RS sym) 1);
 back();
 by (rtac iffI 1);
 (* 1 *)
 by (etac (hd seq.inverts) 1);

 by (etac conjE 1);
 by (etac monofun_cfun_arg 1);
 qed"Cons_inject_less_eq";
 
 goal thy "seq_take (Suc n)`(a>>x) = a>> (seq_take n`x)";
-by (simp_tac (!simpset addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Cons_def]) 1);
 qed"seq_take_Cons";
 
 Addsimps [Cons_not_nil2,Cons_inject_eq,Cons_inject_less_eq,seq_take_Cons,
           Cons_not_UU,Cons_not_less_UU,Cons_not_less_nil,Cons_not_nil];
 

 
 goal thy "!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x";
 by (etac seq.ind 1);
 by (REPEAT (atac 1));
 by (def_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
 qed"Seq_induct";
 
 goal thy "!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |]  \
 \               ==> seq_finite x --> P x";
 by (etac seq_finite_ind 1);
 by (REPEAT (atac 1));
 by (def_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
 qed"Seq_FinitePartial_ind";
 
 goal thy "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x";
 by (etac sfinite.induct 1);
 by (assume_tac 1);
 by (def_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
 qed"Seq_Finite_ind"; 
 
 
 (* rws are definitions to be unfolded for admissibility check *)
 fun Seq_induct_tac s rws i = res_inst_tac [("x",s)] Seq_induct i
                          THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac (i+1))))
-                         THEN simp_tac (!simpset addsimps rws) i;
+                         THEN simp_tac (simpset() addsimps rws) i;
 
 fun Seq_Finite_induct_tac i = etac Seq_Finite_ind i
                               THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac i)));
 
 fun pair_tac s = res_inst_tac [("p",s)] PairE

 (* induction on a sequence of pairs with pairsplitting and simplification *)
 fun pair_induct_tac s rws i = 
            res_inst_tac [("x",s)] Seq_induct i 
            THEN pair_tac "a" (i+3) 
            THEN (REPEAT_DETERM (CHANGED (Simp_tac (i+1)))) 
-           THEN simp_tac (!simpset addsimps rws) i;
+           THEN simp_tac (simpset() addsimps rws) i;
 
 
 
 (* ------------------------------------------------------------------------------------ *)
 
 section "HD,TL";
 
 goal thy "HD`(x>>y) = Def x";
-by (simp_tac (!simpset addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Cons_def]) 1);
 qed"HD_Cons";
 
 goal thy "TL`(x>>y) = y";
-by (simp_tac (!simpset addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Cons_def]) 1);
 qed"TL_Cons";
 
 Addsimps [HD_Cons,TL_Cons];
 
 (* ------------------------------------------------------------------------------------ *)
 
 section "Finite, Partial, Infinite";
 
 goal thy "Finite (a>>xs) = Finite xs";
-by (simp_tac (!simpset addsimps [Cons_def2,Finite_cons]) 1);
+by (simp_tac (simpset() addsimps [Cons_def2,Finite_cons]) 1);
 qed"Finite_Cons";
 
 Addsimps [Finite_Cons];
 goal thy "!! x. Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)";
 by (Seq_Finite_induct_tac 1);

 by (Asm_full_simp_tac 1);
 (* cons *)
 by (strip_tac 1);
 by (Seq_case_simp_tac "x" 1);
 by (Seq_case_simp_tac "y" 1);
-by (SELECT_GOAL (auto_tac (!claset,!simpset))1);
+by (SELECT_GOAL (auto_tac (claset(),simpset()))1);
 by (eres_inst_tac [("x","sa")] allE 1);
 by (eres_inst_tac [("x","y")] allE 1);
 by (Asm_full_simp_tac 1);
 qed"FiniteConc_2";
 

 qed"Map2Finite";
 
 
 goal thy "!! s. Finite s ==> Finite (Filter P`s)";
 by (Seq_Finite_induct_tac 1);
-by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
 qed"FiniteFilter";
 
 
 (* ----------------------------------------------------------------------------------- *)
 

 
 section "Last";
 
 goal thy "!! s. Finite s ==> s~=nil --> Last`s~=UU";
 by (Seq_Finite_induct_tac  1);
-by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
 qed"Finite_Last1";
 
 goal thy "!! s. Finite s ==> Last`s=UU --> s=nil";
 by (Seq_Finite_induct_tac  1);
-by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
 by (fast_tac HOL_cs 1);
 qed"Finite_Last2";
 
 
 (* ------------------------------------------------------------------------------------ *)

 section "Filter, Conc";
 
 
 goal thy "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
 by (Seq_induct_tac "s" [Filter_def] 1);
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
 qed"FilterPQ";
 
 goal thy "Filter P`(x @@ y) = (Filter P`x @@ Filter P`y)";
-by (simp_tac (!simpset addsimps [Filter_def,sfiltersconc]) 1);
+by (simp_tac (simpset() addsimps [Filter_def,sfiltersconc]) 1);
 qed"FilterConc";
 
 (* ------------------------------------------------------------------------------------ *)
 
 section "Map";

 by (Seq_induct_tac "x" [] 1);
 qed"MapConc";
 
 goal thy "Filter P`(Map f`x) = Map f`(Filter (P o f)`x)";
 by (Seq_induct_tac "x" [] 1);
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
 qed"MapFilter";
 
 goal thy "nil = (Map f`s) --> s= nil";
 by (Seq_case_simp_tac "s" 1);
 qed"nilMap";

 
 bind_thm ("ForallTL",ForallTL1 RS mp);
 
 goal thy "Forall P s  --> Forall P (Dropwhile Q`s)";
 by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
-by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
 qed"ForallDropwhile1";
 
 bind_thm ("ForallDropwhile",ForallDropwhile1 RS mp);
 
 

 
 section "Forall, Filter";
 
 
 goal thy "Forall P (Filter P`x)";
-by (simp_tac (!simpset addsimps [Filter_def,Forall_def,forallPsfilterP]) 1);
+by (simp_tac (simpset() addsimps [Filter_def,Forall_def,forallPsfilterP]) 1);
 qed"ForallPFilterP";
 
 (* holds also in other direction, then equal to forallPfilterP *)
 goal thy "Forall P x --> Filter P`x = x";
 by (Seq_induct_tac "x" [Forall_def,sforall_def,Filter_def] 1);

 by (rtac adm_all 1);
 (* base cases *)
 by (Simp_tac 1);
 by (Simp_tac 1);
 (* main case *)
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
 qed"FilternPnilForallP1";
 
 bind_thm ("FilternPnilForallP",FilternPnilForallP1 RS mp);
 
 (* inverse of ForallnPFilterPUU. proved by 2 lemmas because of adm problems *)
 
 goal thy "!! ys. Finite ys ==> Filter P`ys ~= UU";
 by (Seq_Finite_induct_tac 1);
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
 qed"FilterUU_nFinite_lemma1";
 
 goal thy "~ Forall (%x. ~P x) ys --> Filter P`ys ~= UU";
 by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
 qed"FilterUU_nFinite_lemma2";
 
 goal thy   "!! P. Filter P`ys = UU ==> \
 \                (Forall (%x. ~P x) ys  & ~Finite ys)";
 by (rtac conjI 1);
 by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1);
 by (Auto_tac());
-by (blast_tac (!claset addSDs [FilterUU_nFinite_lemma1]) 1);
+by (blast_tac (claset() addSDs [FilterUU_nFinite_lemma1]) 1);
 qed"FilternPUUForallP";
 
 
 goal thy  "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|] \
 \   ==> Filter P`ys = nil";

 
 section "Takewhile, Forall, Filter";
 
 
 goal thy "Forall P (Takewhile P`x)";
-by (simp_tac (!simpset addsimps [Forall_def,Takewhile_def,sforallPstakewhileP]) 1);
+by (simp_tac (simpset() addsimps [Forall_def,Takewhile_def,sforallPstakewhileP]) 1);
 qed"ForallPTakewhileP";
 
 
 goal thy"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q`x)";
 by (rtac ForallPForallQ 1);

 Addsimps [ForallPTakewhileP,ForallPTakewhileQ,
           FilterPTakewhileQnil,FilterPTakewhileQid];
 
 goal thy "Takewhile P`(Takewhile P`s) = Takewhile P`s";
 by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
-by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
 qed"Takewhile_idempotent";
 
 goal thy "Forall P s --> Takewhile (%x. Q x | (~P x))`s = Takewhile Q`s";
 by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
 qed"ForallPTakewhileQnP";

 
 
 goal thy "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 = seq_take k`y2|] \
 \ ==> seq_take n`(x @@ (s>>y1)) =  seq_take n`(y @@ (t>>y2))";
 
-by (auto_tac (!claset addSIs [take_reduction1 RS spec RS mp],!simpset));
+by (auto_tac (claset() addSIs [take_reduction1 RS spec RS mp],simpset()));
 qed"take_reduction";
 
 (* ------------------------------------------------------------------
           take-lemma and take_reduction for << instead of = 
    ------------------------------------------------------------------ *)

 qed"take_reduction_less1";
 
 
 goal thy "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 << seq_take k`y2|] \
 \ ==> seq_take n`(x @@ (s>>y1)) <<  seq_take n`(y @@ (t>>y2))";
-by (auto_tac (!claset addSIs [take_reduction_less1 RS spec RS mp],!simpset));
+by (auto_tac (claset() addSIs [take_reduction_less1 RS spec RS mp],simpset()));
 qed"take_reduction_less";
 
 
 val prems = goalw thy [seq.take_def]
 "(!! n. seq_take n`s1 << seq_take n`s2)  ==> s1<<s2";

 goal thy "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
 \           !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] \
 \                         ==> (f (s1 @@ y>>s2)) = (g (s1 @@ y>>s2)) |] \
 \              ==> A x --> (f x)=(g x)";
 by (case_tac "Forall Q x" 1);
-by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
 qed"take_lemma_principle1";
 
 goal thy "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
 \           !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] \
 \                         ==> ! n. seq_take n`(f (s1 @@ y>>s2)) \
 \                                = seq_take n`(g (s1 @@ y>>s2)) |] \
 \              ==> A x --> (f x)=(g x)";
 by (case_tac "Forall Q x" 1);
-by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
 by (resolve_tac seq.take_lemmas 1);
 by (Auto_tac());
 qed"take_lemma_principle2";
 
 

 by (res_inst_tac [("x","x")] spec 1);
 by (rtac nat_induct 1);
 by (Simp_tac 1);
 by (rtac allI 1);
 by (case_tac "Forall Q xa" 1);
-by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
-                           !simpset)) 1);
-by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
+                           simpset())) 1);
+by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
 qed"take_lemma_induct";
 
 
 goal thy 
 "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \

 by (assume_tac 2);
 by (res_inst_tac [("x","x")] spec 1);
 by (rtac less_induct 1);
 by (rtac allI 1);
 by (case_tac "Forall Q xa" 1);
-by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
-                           !simpset)) 1);
-by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
+                           simpset())) 1);
+by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
 qed"take_lemma_less_induct";
 
 
 (*
 local

 by (res_inst_tac [("x","h1a")] spec 1);
 by (res_inst_tac [("x","x")] spec 1);
 by (rtac less_induct 1);
 by (rtac allI 1);
 by (case_tac "Forall Q xa" 1);
-by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
-                           !simpset)) 1);
-by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
+                           simpset())) 1);
+by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
 qed"take_lemma_less_induct";
 
 
 
 goal thy 

 FIX
 
 by (rtac less_induct 1);
 by (rtac allI 1);
 by (case_tac "Forall Q xa" 1);
-by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
-                           !simpset)) 1);
-by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
+                           simpset())) 1);
+by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
 qed"take_lemma_less_induct";
 
 
 *)
 

 goal thy "Forall (%x.~(P x & Q x)) s \
 \         --> Filter P`(Filter Q`s) =\
 \             Filter (%x. P x & Q x)`s";
 
 by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
 qed"Filter_lemma1";
 
 goal thy "!! s. Finite s ==>  \
 \         (Forall (%x. (~P x) | (~ Q x)) s  \
 \         --> Filter P`(Filter Q`s) = nil)";
 by (Seq_Finite_induct_tac 1);
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
 qed"Filter_lemma2";
 
 goal thy "!! s. Finite s ==>  \
 \         Forall (%x. (~P x) | (~ Q x)) s  \
 \         --> Filter (%x. P x & Q x)`s = nil";
 by (Seq_Finite_induct_tac 1);
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
 qed"Filter_lemma3";
 
 
 goal thy "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
 by (res_inst_tac [("A1","%x. True") 
                  ,("Q1","%x.~(P x & Q x)"),("x1","s")]
                  (take_lemma_induct RS mp) 1);
 (* FIX: better support for A = %x. True *)
 by (Fast_tac 3);
-by (asm_full_simp_tac (!simpset addsimps [Filter_lemma1]) 1);
-by (asm_full_simp_tac (!simpset addsimps [Filter_lemma2,Filter_lemma3] 
+by (asm_full_simp_tac (simpset() addsimps [Filter_lemma1]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Filter_lemma2,Filter_lemma3] 
                                 setloop split_tac [expand_if]) 1);
 qed"FilterPQ_takelemma";
 
 Addsimps [FilterPQ];