isatool fixclasimp;
authorwenzelm
Mon Nov 03 14:06:27 1997 +0100 (1997-11-03)
changeset 409871e05eb27fb6
parent 4097 ddd1c18121e0
child 4099 0ec0d2dbe3f4
isatool fixclasimp;
src/HOLCF/Cfun2.ML
src/HOLCF/Cfun3.ML
src/HOLCF/Cont.ML
src/HOLCF/Cprod2.ML
src/HOLCF/Cprod3.ML
src/HOLCF/Discrete.ML
src/HOLCF/Discrete1.ML
src/HOLCF/Fix.ML
src/HOLCF/Fun2.ML
src/HOLCF/HOLCF.ML
src/HOLCF/IMP/Denotational.ML
src/HOLCF/IMP/HoareEx.ML
src/HOLCF/IOA/ABP/Correctness.ML
src/HOLCF/IOA/ABP/Lemmas.ML
src/HOLCF/IOA/NTP/Abschannel.ML
src/HOLCF/IOA/NTP/Correctness.ML
src/HOLCF/IOA/NTP/Impl.ML
src/HOLCF/IOA/NTP/Lemmas.ML
src/HOLCF/IOA/NTP/Multiset.ML
src/HOLCF/IOA/NTP/Packet.ML
src/HOLCF/IOA/NTP/Receiver.ML
src/HOLCF/IOA/NTP/Sender.ML
src/HOLCF/IOA/meta_theory/Asig.ML
src/HOLCF/IOA/meta_theory/Automata.ML
src/HOLCF/IOA/meta_theory/CompoExecs.ML
src/HOLCF/IOA/meta_theory/CompoScheds.ML
src/HOLCF/IOA/meta_theory/CompoTraces.ML
src/HOLCF/IOA/meta_theory/Compositionality.ML
src/HOLCF/IOA/meta_theory/Deadlock.ML
src/HOLCF/IOA/meta_theory/RefCorrectness.ML
src/HOLCF/IOA/meta_theory/RefMappings.ML
src/HOLCF/IOA/meta_theory/Seq.ML
src/HOLCF/IOA/meta_theory/Sequence.ML
src/HOLCF/IOA/meta_theory/ShortExecutions.ML
src/HOLCF/IOA/meta_theory/Traces.ML
src/HOLCF/Lift.ML
src/HOLCF/Lift2.ML
src/HOLCF/Lift3.ML
src/HOLCF/One.ML
src/HOLCF/Pcpo.ML
src/HOLCF/Porder.ML
src/HOLCF/Sprod3.ML
src/HOLCF/Ssum0.ML
src/HOLCF/Ssum2.ML
src/HOLCF/Ssum3.ML
src/HOLCF/Tr.ML
src/HOLCF/Up1.ML
src/HOLCF/Up2.ML
src/HOLCF/Up3.ML
src/HOLCF/domain/theorems.ML
src/HOLCF/ex/Dagstuhl.ML
src/HOLCF/ex/Dnat.ML
src/HOLCF/ex/Hoare.ML
src/HOLCF/ex/Loop.ML
src/HOLCF/ex/Stream.ML
     1.1 --- a/src/HOLCF/Cfun2.ML	Mon Nov 03 12:36:48 1997 +0100
     1.2 +++ b/src/HOLCF/Cfun2.ML	Mon Nov 03 14:06:27 1997 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4  qed_goal "less_cfun" thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
     1.5  (fn prems =>
     1.6          [
     1.7 -        (simp_tac (!simpset addsimps [inst_cfun_po]) 1)
     1.8 +        (simp_tac (simpset() addsimps [inst_cfun_po]) 1)
     1.9          ]);
    1.10  
    1.11  (* ------------------------------------------------------------------------ *)
     2.1 --- a/src/HOLCF/Cfun3.ML	Mon Nov 03 12:36:48 1997 +0100
     2.2 +++ b/src/HOLCF/Cfun3.ML	Mon Nov 03 14:06:27 1997 +0100
     2.3 @@ -339,7 +339,7 @@
     2.4  
     2.5  qed_goalw "strictify1" thy [strictify_def] "strictify`f`UU=UU" (fn _ => [
     2.6          (stac beta_cfun 1),
     2.7 -         (simp_tac (!simpset addsimps [cont_Istrictify2,cont_Istrictify1,
     2.8 +         (simp_tac (simpset() addsimps [cont_Istrictify2,cont_Istrictify1,
     2.9  					cont2cont_CF1L]) 1),
    2.10          (stac beta_cfun 1),
    2.11          (rtac cont_Istrictify2 1),
    2.12 @@ -349,7 +349,7 @@
    2.13  qed_goalw "strictify2" thy [strictify_def]
    2.14          "~x=UU ==> strictify`f`x=f`x"  (fn prems => [
    2.15          (stac beta_cfun 1),
    2.16 -         (simp_tac (!simpset addsimps [cont_Istrictify2,cont_Istrictify1,
    2.17 +         (simp_tac (simpset() addsimps [cont_Istrictify2,cont_Istrictify1,
    2.18  					cont2cont_CF1L]) 1),
    2.19          (stac beta_cfun 1),
    2.20          (rtac cont_Istrictify2 1),
    2.21 @@ -370,7 +370,7 @@
    2.22  (* ------------------------------------------------------------------------ *)
    2.23  
    2.24  (* HINT: cont_tac is now installed in simplifier in Lift.ML ! *)
    2.25 -(*simpset := !simpset addsolver (K (DEPTH_SOLVE_1 o cont_tac));*)
    2.26 +(*simpset_ref() := simpset() addsolver (K (DEPTH_SOLVE_1 o cont_tac));*)
    2.27  
    2.28  (* ------------------------------------------------------------------------ *)
    2.29  (* some lemmata for functions with flat/chain_finite domain/range types	    *)
     3.1 --- a/src/HOLCF/Cont.ML	Mon Nov 03 12:36:48 1997 +0100
     3.2 +++ b/src/HOLCF/Cont.ML	Mon Nov 03 14:06:27 1997 +0100
     3.3 @@ -666,7 +666,7 @@
     3.4  	cut_facts_tac prems 1,
     3.5  	strip_tac 1,
     3.6  	dtac (ax_flat RS spec RS spec RS mp) 1,
     3.7 -	fast_tac ((HOL_cs addss (!simpset addsimps [minimal]))) 1
     3.8 +	fast_tac ((HOL_cs addss (simpset() addsimps [minimal]))) 1
     3.9  	]);
    3.10  
    3.11  
     4.1 --- a/src/HOLCF/Cprod2.ML	Mon Nov 03 12:36:48 1997 +0100
     4.2 +++ b/src/HOLCF/Cprod2.ML	Mon Nov 03 14:06:27 1997 +0100
     4.3 @@ -40,7 +40,7 @@
     4.4  qed_goal "minimal_cprod" thy  "(UU,UU)<<p"
     4.5  (fn prems =>
     4.6          [
     4.7 -        (simp_tac(!simpset addsimps[inst_cprod_po])1)
     4.8 +        (simp_tac(simpset() addsimps[inst_cprod_po])1)
     4.9          ]);
    4.10  
    4.11  bind_thm ("UU_cprod_def",minimal_cprod RS minimal2UU RS sym);
    4.12 @@ -62,13 +62,13 @@
    4.13          (strip_tac 1),
    4.14          (rtac (less_fun RS iffD2) 1),
    4.15          (strip_tac 1),
    4.16 -        (asm_simp_tac (!simpset addsimps [inst_cprod_po]) 1)
    4.17 +        (asm_simp_tac (simpset() addsimps [inst_cprod_po]) 1)
    4.18          ]);
    4.19  
    4.20  qed_goalw "monofun_pair2" thy [monofun] "monofun(Pair x)"
    4.21   (fn prems =>
    4.22          [
    4.23 -        (asm_simp_tac (!simpset addsimps [inst_cprod_po]) 1)
    4.24 +        (asm_simp_tac (simpset() addsimps [inst_cprod_po]) 1)
    4.25          ]);
    4.26  
    4.27  qed_goal "monofun_pair" thy "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)"
     5.1 --- a/src/HOLCF/Cprod3.ML	Mon Nov 03 12:36:48 1997 +0100
     5.2 +++ b/src/HOLCF/Cprod3.ML	Mon Nov 03 14:06:27 1997 +0100
     5.3 @@ -155,7 +155,7 @@
     5.4   (fn prems =>
     5.5          [
     5.6          (stac beta_cfun 1),
     5.7 -        (simp_tac (!simpset addsimps [cont_pair1,cont_pair2,cont2cont_CF1L]) 1),
     5.8 +        (simp_tac (simpset() addsimps [cont_pair1,cont_pair2,cont2cont_CF1L]) 1),
     5.9          (stac beta_cfun 1),
    5.10          (rtac cont_pair2 1),
    5.11          (rtac refl 1)
    5.12 @@ -287,7 +287,7 @@
    5.13          [
    5.14          (stac beta_cfun 1),
    5.15          (Simp_tac 1),
    5.16 -        (simp_tac (!simpset addsimps [cfst2,csnd2]) 1)
    5.17 +        (simp_tac (simpset() addsimps [cfst2,csnd2]) 1)
    5.18          ]);
    5.19  
    5.20  qed_goalw "csplit3" Cprod3.thy [csplit_def]
    5.21 @@ -296,7 +296,7 @@
    5.22          [
    5.23          (stac beta_cfun 1),
    5.24          (Simp_tac 1),
    5.25 -        (simp_tac (!simpset addsimps [surjective_pairing_Cprod2]) 1)
    5.26 +        (simp_tac (simpset() addsimps [surjective_pairing_Cprod2]) 1)
    5.27          ]);
    5.28  
    5.29  (* ------------------------------------------------------------------------ *)
     6.1 --- a/src/HOLCF/Discrete.ML	Mon Nov 03 12:36:48 1997 +0100
     6.2 +++ b/src/HOLCF/Discrete.ML	Mon Nov 03 14:06:27 1997 +0100
     6.3 @@ -11,10 +11,10 @@
     6.4  
     6.5  goal thy
     6.6   "!!S::nat=>('a::term)discr. is_chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
     6.7 -by(fast_tac (!claset addDs [discr_chain0] addEs [arg_cong]) 1);
     6.8 +by(fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1);
     6.9  qed "discr_chain_f_range0";
    6.10  
    6.11  goalw thy [cont,is_lub,is_ub] "cont(%x::('a::term)discr. f x)";
    6.12 -by(simp_tac (!simpset addsimps [discr_chain_f_range0]) 1);
    6.13 +by(simp_tac (simpset() addsimps [discr_chain_f_range0]) 1);
    6.14  qed "cont_discr";
    6.15  AddIffs [cont_discr];
     7.1 --- a/src/HOLCF/Discrete1.ML	Mon Nov 03 12:36:48 1997 +0100
     7.2 +++ b/src/HOLCF/Discrete1.ML	Mon Nov 03 14:06:27 1997 +0100
     7.3 @@ -22,7 +22,7 @@
     7.4  
     7.5  goal thy
     7.6   "!!S::nat=>('a::term)discr. is_chain(S) ==> range(S) = {S 0}";
     7.7 -by (fast_tac (!claset addEs [discr_chain0]) 1);
     7.8 +by (fast_tac (claset() addEs [discr_chain0]) 1);
     7.9  qed "discr_chain_range0";
    7.10  Addsimps [discr_chain_range0];
    7.11  
     8.1 --- a/src/HOLCF/Fix.ML	Mon Nov 03 12:36:48 1997 +0100
     8.2 +++ b/src/HOLCF/Fix.ML	Mon Nov 03 14:06:27 1997 +0100
     8.3 @@ -330,7 +330,7 @@
     8.4  qed_goalw "fix_eq" thy  [fix_def] "fix`F = F`(fix`F)"
     8.5   (fn prems =>
     8.6          [
     8.7 -        (asm_simp_tac (!simpset addsimps [cont_Ifix]) 1),
     8.8 +        (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1),
     8.9          (rtac Ifix_eq 1)
    8.10          ]);
    8.11  
    8.12 @@ -338,7 +338,7 @@
    8.13   (fn prems =>
    8.14          [
    8.15          (cut_facts_tac prems 1),
    8.16 -        (asm_simp_tac (!simpset addsimps [cont_Ifix]) 1),
    8.17 +        (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1),
    8.18          (etac Ifix_least 1)
    8.19          ]);
    8.20  
    8.21 @@ -439,7 +439,7 @@
    8.22   (fn prems =>
    8.23          [
    8.24          (fold_goals_tac [Ifix_def]),
    8.25 -        (asm_simp_tac (!simpset addsimps [cont_Ifix]) 1)
    8.26 +        (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1)
    8.27          ]);
    8.28  
    8.29  
    8.30 @@ -563,7 +563,7 @@
    8.31  	strip_tac 1,
    8.32  	dtac chfin_fappR 1,
    8.33  	eres_inst_tac [("x","s")] allE 1,
    8.34 -	fast_tac (HOL_cs addss (!simpset addsimps [chfin])) 1]);
    8.35 +	fast_tac (HOL_cs addss (simpset() addsimps [chfin])) 1]);
    8.36  
    8.37  (* adm_flat not needed any more, since it is a special case of adm_chfindom *)
    8.38  
    8.39 @@ -670,7 +670,7 @@
    8.40  
    8.41  qed_goal "adm_eq"  thy 
    8.42          "!!u. [|cont u ; cont v|]==> adm(%x. u x = v x)"
    8.43 - (fn prems => [asm_simp_tac (!simpset addsimps [po_eq_conv]) 1]);
    8.44 + (fn prems => [asm_simp_tac (simpset() addsimps [po_eq_conv]) 1]);
    8.45  
    8.46  
    8.47  
    8.48 @@ -691,13 +691,13 @@
    8.49    val adm_disj_lemma2 = prove_goal thy  
    8.50    "!!Q. [| adm(Q); ? X. is_chain(X) & (!n. Q(X(n))) &\
    8.51    \   lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"
    8.52 - (fn _ => [fast_tac (!claset addEs [admD] addss !simpset) 1]);
    8.53 + (fn _ => [fast_tac (claset() addEs [admD] addss simpset()) 1]);
    8.54  
    8.55    val adm_disj_lemma3 = prove_goalw thy [is_chain]
    8.56    "!!Q. is_chain(Y) ==> is_chain(%m. if m < Suc i then Y(Suc i) else Y m)"
    8.57   (fn _ =>
    8.58          [
    8.59 -        asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1,
    8.60 +        asm_simp_tac (simpset() setloop (split_tac[expand_if])) 1,
    8.61          safe_tac HOL_cs,
    8.62          subgoal_tac "ia = i" 1,
    8.63          Asm_simp_tac 1,
    8.64 @@ -708,7 +708,7 @@
    8.65    "!!Q. !j. i < j --> Q(Y(j))  ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)"
    8.66   (fn _ =>
    8.67          [
    8.68 -        asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1,
    8.69 +        asm_simp_tac (simpset() setloop (split_tac[expand_if])) 1,
    8.70          strip_tac 1,
    8.71          etac allE 1,
    8.72          etac mp 1,
    8.73 @@ -722,7 +722,7 @@
    8.74          [
    8.75          safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3]),
    8.76          atac 2,
    8.77 -        asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1,
    8.78 +        asm_simp_tac (simpset() setloop (split_tac[expand_if])) 1,
    8.79          res_inst_tac [("x","i")] exI 1,
    8.80          strip_tac 1,
    8.81          trans_tac 1
     9.1 --- a/src/HOLCF/Fun2.ML	Mon Nov 03 12:36:48 1997 +0100
     9.2 +++ b/src/HOLCF/Fun2.ML	Mon Nov 03 14:06:27 1997 +0100
     9.3 @@ -23,7 +23,7 @@
     9.4  qed_goal "minimal_fun" thy "(%z. UU) << x"
     9.5  (fn prems =>
     9.6          [
     9.7 -        (simp_tac (!simpset addsimps [inst_fun_po,minimal]) 1)
     9.8 +        (simp_tac (simpset() addsimps [inst_fun_po,minimal]) 1)
     9.9          ]);
    9.10  
    9.11  bind_thm ("UU_fun_def",minimal_fun RS minimal2UU RS sym);
    10.1 --- a/src/HOLCF/HOLCF.ML	Mon Nov 03 12:36:48 1997 +0100
    10.2 +++ b/src/HOLCF/HOLCF.ML	Mon Nov 03 14:06:27 1997 +0100
    10.3 @@ -8,7 +8,7 @@
    10.4  
    10.5  use"adm.ML";
    10.6  
    10.7 -simpset := !simpset addSolver(fn thms =>
    10.8 +simpset_ref() := simpset() addSolver(fn thms =>
    10.9              (adm_tac (cut_facts_tac thms THEN' cont_tacRs)));
   10.10  
   10.11 -val HOLCF_ss = !simpset;
   10.12 +val HOLCF_ss = simpset();
    11.1 --- a/src/HOLCF/IMP/Denotational.ML	Mon Nov 03 12:36:48 1997 +0100
    11.2 +++ b/src/HOLCF/IMP/Denotational.ML	Mon Nov 03 14:06:27 1997 +0100
    11.3 @@ -18,7 +18,7 @@
    11.4  
    11.5  goalw thy [dlift_def]
    11.6   "(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)";
    11.7 -by (simp_tac (!simpset setloop (split_tac[expand_lift_case])) 1);
    11.8 +by (simp_tac (simpset() setloop (split_tac[expand_lift_case])) 1);
    11.9  qed "dlift_is_Def";
   11.10  Addsimps [dlift_is_Def];
   11.11  
   11.12 @@ -30,19 +30,19 @@
   11.13  
   11.14  goal thy "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t";
   11.15  by (com.induct_tac "c" 1);
   11.16 -    by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
   11.17 -   by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
   11.18 -  by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
   11.19 - by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   11.20 - by (fast_tac ((HOL_cs addIs evalc.intrs) addss !simpset) 1);
   11.21 +    by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
   11.22 +   by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
   11.23 +  by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
   11.24 + by (simp_tac (simpset() setloop (split_tac[expand_if])) 1);
   11.25 + by (fast_tac ((HOL_cs addIs evalc.intrs) addss simpset()) 1);
   11.26  by (Simp_tac 1);
   11.27  by (rtac fix_ind 1);
   11.28    by (fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,ax_flat_lift])) 1);
   11.29   by (Simp_tac 1);
   11.30 -by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   11.31 +by (simp_tac (simpset() setloop (split_tac[expand_if])) 1);
   11.32  by (safe_tac HOL_cs);
   11.33    by (fast_tac (HOL_cs addIs evalc.intrs) 1);
   11.34 - by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
   11.35 + by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
   11.36  qed_spec_mp "D_implies_eval";
   11.37  
   11.38  
    12.1 --- a/src/HOLCF/IMP/HoareEx.ML	Mon Nov 03 12:36:48 1997 +0100
    12.2 +++ b/src/HOLCF/IMP/HoareEx.ML	Mon Nov 03 14:06:27 1997 +0100
    12.3 @@ -14,6 +14,6 @@
    12.4    (* simplifier with enhanced adm-tactic: *)
    12.5    by (Simp_tac 1);
    12.6   by (Simp_tac 1);
    12.7 -by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
    12.8 +by (simp_tac (simpset() setloop (split_tac[expand_if])) 1);
    12.9  by(Blast_tac 1);
   12.10  qed "WHILE_rule_sound";
    13.1 --- a/src/HOLCF/IOA/ABP/Correctness.ML	Mon Nov 03 12:36:48 1997 +0100
    13.2 +++ b/src/HOLCF/IOA/ABP/Correctness.ML	Mon Nov 03 14:06:27 1997 +0100
    13.3 @@ -83,7 +83,7 @@
    13.4  by (List.list.induct_tac "l" 1);
    13.5  by (Simp_tac 1);
    13.6  by (case_tac "list =[]" 1);
    13.7 -by (asm_full_simp_tac (!simpset addsimps [reverse_Cons]) 1);
    13.8 +by (asm_full_simp_tac (simpset() addsimps [reverse_Cons]) 1);
    13.9  (* main case *)
   13.10  by (rotate 1 1);
   13.11  by (Asm_full_simp_tac 1);
   13.12 @@ -93,7 +93,7 @@
   13.13  by (Asm_simp_tac 1);
   13.14  by (rtac (expand_if RS ssubst) 1);
   13.15  by (hyp_subst_tac 1);
   13.16 -by (asm_full_simp_tac (!simpset addsimps [reverse_Cons]) 1); 
   13.17 +by (asm_full_simp_tac (simpset() addsimps [reverse_Cons]) 1); 
   13.18  qed"rev_red_not_nil";
   13.19  
   13.20  (* shows applicability of the induction hypothesis of the following Lemma 1 *)
   13.21 @@ -109,7 +109,7 @@
   13.22                            (rev_red_not_nil RS mp)])  1);
   13.23  qed"last_ind_on_first";
   13.24  
   13.25 -val impl_ss = !simpset delsimps [reduce_Cons];
   13.26 +val impl_ss = simpset() delsimps [reduce_Cons];
   13.27  
   13.28  (* Main Lemma 1 for S_pkt in showing that reduce is refinement  *) 
   13.29  goal Correctness.thy 
   13.30 @@ -122,7 +122,7 @@
   13.31  by (List.list.induct_tac "l" 1);
   13.32  by (Simp_tac 1);
   13.33  by (case_tac "list=[]" 1);
   13.34 - by (asm_full_simp_tac (!simpset addsimps [reverse_Nil,reverse_Cons]) 1);
   13.35 + by (asm_full_simp_tac (simpset() addsimps [reverse_Nil,reverse_Cons]) 1);
   13.36   by (rtac impI 1);
   13.37  by (Simp_tac 1);
   13.38  by (cut_inst_tac [("l","list")] cons_not_nil 1);
   13.39 @@ -131,16 +131,16 @@
   13.40   by (hyp_subst_tac 1);
   13.41  by (asm_full_simp_tac (impl_ss addsimps [last_ind_on_first,l_iff_red_nil]) 1);
   13.42  (* <-- *)
   13.43 -by (simp_tac (!simpset addsimps [and_de_morgan_and_absorbe,l_iff_red_nil]) 1);
   13.44 +by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe,l_iff_red_nil]) 1);
   13.45  by (List.list.induct_tac "l" 1);
   13.46  by (Simp_tac 1);
   13.47  by (case_tac "list=[]" 1);
   13.48  by (cut_inst_tac [("l","list")] cons_not_nil 2);
   13.49 -by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
   13.50 -by (auto_tac (!claset, 
   13.51 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
   13.52 +by (auto_tac (claset(), 
   13.53  	      impl_ss addsimps [last_ind_on_first,l_iff_red_nil] 
   13.54                        setloop split_tac [expand_if]));
   13.55 -by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
   13.56 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
   13.57  qed"reduce_hd";
   13.58  
   13.59  
   13.60 @@ -156,7 +156,7 @@
   13.61  by (Asm_full_simp_tac 1);
   13.62  by (rtac (expand_if RS ssubst) 1);
   13.63  by (rtac conjI 1);
   13.64 -by (simp_tac (!simpset addsimps [and_de_morgan_and_absorbe]) 2);
   13.65 +by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe]) 2);
   13.66  by (Step_tac 1);
   13.67  by (ALLGOALS (cut_inst_tac [("l","xs")] cons_not_nil));
   13.68  by (Auto_tac());
   13.69 @@ -169,13 +169,13 @@
   13.70  
   13.71  goal Correctness.thy 
   13.72        "is_weak_ref_map reduce ch_ioa ch_fin_ioa";
   13.73 -by (simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
   13.74 +by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
   13.75  (* ---------------- main-part ------------------- *)
   13.76  by (REPEAT (rtac allI 1));
   13.77  by (rtac imp_conj_lemma 1);
   13.78  by (abs_action.induct_tac "a" 1);
   13.79  (* ----------------- 2 cases ---------------------*)
   13.80 -by (ALLGOALS (simp_tac (!simpset addsimps [externals_def])));
   13.81 +by (ALLGOALS (simp_tac (simpset() addsimps [externals_def])));
   13.82  (* fst case --------------------------------------*)
   13.83   by (rtac impI 1);
   13.84   by (rtac disjI2 1);
   13.85 @@ -184,9 +184,9 @@
   13.86   by (rtac impI 1);
   13.87   by (REPEAT (etac conjE 1));
   13.88   by (etac disjE 1);
   13.89 -by (asm_full_simp_tac (!simpset addsimps [l_iff_red_nil]) 1);
   13.90 +by (asm_full_simp_tac (simpset() addsimps [l_iff_red_nil]) 1);
   13.91  by (etac (hd_is_reduce_hd RS mp) 1); 
   13.92 -by (asm_full_simp_tac (!simpset addsimps [l_iff_red_nil]) 1);
   13.93 +by (asm_full_simp_tac (simpset() addsimps [l_iff_red_nil]) 1);
   13.94  by (rtac conjI 1);
   13.95  by (etac (hd_is_reduce_hd RS mp) 1); 
   13.96  by (rtac (bool_if_impl_or RS mp) 1);
   13.97 @@ -210,7 +210,7 @@
   13.98     the absence of internal actions. *)
   13.99  goal Correctness.thy 
  13.100        "is_weak_ref_map (%id. id) sender_ioa sender_ioa";
  13.101 -by (simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
  13.102 +by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
  13.103  by (TRY(
  13.104     (rtac conjI 1) THEN
  13.105  (* start states *)
  13.106 @@ -220,13 +220,13 @@
  13.107  by (rtac imp_conj_lemma 1);
  13.108  by (Action.action.induct_tac "a" 1);
  13.109  (* 7 cases *)
  13.110 -by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if]))));
  13.111 +by (ALLGOALS (simp_tac ((simpset() addsimps [externals_def]) setloop (split_tac [expand_if]))));
  13.112  qed"sender_unchanged";
  13.113  
  13.114  (* 2 copies of before *)
  13.115  goal Correctness.thy 
  13.116        "is_weak_ref_map (%id. id) receiver_ioa receiver_ioa";
  13.117 -by (simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
  13.118 +by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
  13.119  by (TRY(
  13.120     (rtac conjI 1) THEN
  13.121   (* start states *)
  13.122 @@ -236,12 +236,12 @@
  13.123  by (rtac imp_conj_lemma 1);
  13.124  by (Action.action.induct_tac "a" 1);
  13.125  (* 7 cases *)
  13.126 -by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if]))));
  13.127 +by (ALLGOALS (simp_tac ((simpset() addsimps [externals_def]) setloop (split_tac [expand_if]))));
  13.128  qed"receiver_unchanged";
  13.129  
  13.130  goal Correctness.thy 
  13.131        "is_weak_ref_map (%id. id) env_ioa env_ioa";
  13.132 -by (simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
  13.133 +by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
  13.134  by (TRY(
  13.135     (rtac conjI 1) THEN
  13.136  (* start states *)
  13.137 @@ -251,11 +251,11 @@
  13.138  by (rtac imp_conj_lemma 1);
  13.139  by (Action.action.induct_tac "a" 1);
  13.140  (* 7 cases *)
  13.141 -by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if]))));
  13.142 +by (ALLGOALS (simp_tac ((simpset() addsimps [externals_def]) setloop (split_tac [expand_if]))));
  13.143  qed"env_unchanged";
  13.144  
  13.145  goal Correctness.thy "compatible srch_ioa rsch_ioa"; 
  13.146 -by (simp_tac (!simpset addsimps [compatible_def,Int_def,empty_def]) 1);
  13.147 +by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
  13.148  by (rtac set_ext 1);
  13.149  by (Action.action.induct_tac "x" 1);
  13.150  by (ALLGOALS(Simp_tac));
  13.151 @@ -263,14 +263,14 @@
  13.152  
  13.153  (* totally the same as before *)
  13.154  goal Correctness.thy "compatible srch_fin_ioa rsch_fin_ioa"; 
  13.155 -by (simp_tac (!simpset addsimps [compatible_def,Int_def,empty_def]) 1);
  13.156 +by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
  13.157  by (rtac set_ext 1);
  13.158  by (Action.action.induct_tac "x" 1);
  13.159  by (ALLGOALS(Simp_tac));
  13.160  val compat_single_fin_ch = result();
  13.161  
  13.162  val ss =
  13.163 -  !simpset delsimps ([trans_of_def, srch_asig_def,rsch_asig_def,
  13.164 +  simpset() delsimps ([trans_of_def, srch_asig_def,rsch_asig_def,
  13.165                        asig_of_def, actions_def, srch_trans_def, rsch_trans_def,
  13.166                        srch_ioa_def, srch_fin_ioa_def, rsch_fin_ioa_def, 
  13.167                        rsch_ioa_def, Sender.sender_trans_def,
  13.168 @@ -336,7 +336,7 @@
  13.169  goal Correctness.thy 
  13.170   "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) &  \
  13.171  \ externals(asig_of(rsch_fin_ioa)) = externals(asig_of(rsch_ioa))";
  13.172 -   by (simp_tac (!simpset addsimps [externals_def]) 1);
  13.173 +   by (simp_tac (simpset() addsimps [externals_def]) 1);
  13.174  val ext_single_ch = result();
  13.175  
  13.176  
  13.177 @@ -354,7 +354,7 @@
  13.178              S o u n d n e s s   o f   A b s t r a c t i o n        
  13.179  *************************************************************************)
  13.180  
  13.181 -val ss = !simpset delsimps ([asig_of_def, srch_ioa_def, rsch_ioa_def,
  13.182 +val ss = simpset() delsimps ([asig_of_def, srch_ioa_def, rsch_ioa_def,
  13.183                               srch_fin_ioa_def, rsch_fin_ioa_def] @
  13.184                              impl_ioas @ env_ioas);
  13.185  
    14.1 --- a/src/HOLCF/IOA/ABP/Lemmas.ML	Mon Nov 03 12:36:48 1997 +0100
    14.2 +++ b/src/HOLCF/IOA/ABP/Lemmas.ML	Mon Nov 03 14:06:27 1997 +0100
    14.3 @@ -8,7 +8,7 @@
    14.4  (* Logic *)
    14.5  
    14.6  val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    14.7 -  by(fast_tac (!claset addDs prems) 1);
    14.8 +  by(fast_tac (claset() addDs prems) 1);
    14.9  qed "imp_conj_lemma";
   14.10  
   14.11  goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)";
   14.12 @@ -42,7 +42,7 @@
   14.13  
   14.14  (* Lists *)
   14.15  
   14.16 -val list_ss = simpset_of "List";
   14.17 +val list_ss = simpset_of List.thy;
   14.18  
   14.19  goal List.thy "hd(l@m) = (if l~=[] then hd(l) else hd(m))";
   14.20  by (List.list.induct_tac "l" 1);
    15.1 --- a/src/HOLCF/IOA/NTP/Abschannel.ML	Mon Nov 03 12:36:48 1997 +0100
    15.2 +++ b/src/HOLCF/IOA/NTP/Abschannel.ML	Mon Nov 03 14:06:27 1997 +0100
    15.3 @@ -25,7 +25,7 @@
    15.4       \ C_m_r ~: actions(srch_asig)           &    \
    15.5       \ C_r_s ~: actions(srch_asig)  & C_r_r(m) ~: actions(srch_asig)";
    15.6  
    15.7 -by(simp_tac (!simpset addsimps unfold_renaming) 1);
    15.8 +by(simp_tac (simpset() addsimps unfold_renaming) 1);
    15.9  qed"in_srch_asig";
   15.10  
   15.11  goal Abschannel.thy
   15.12 @@ -40,20 +40,20 @@
   15.13       \ C_r_s ~: actions(rsch_asig)            & \
   15.14       \ C_r_r(m) ~: actions(rsch_asig)";
   15.15  
   15.16 -by(simp_tac (!simpset addsimps unfold_renaming) 1);
   15.17 +by(simp_tac (simpset() addsimps unfold_renaming) 1);
   15.18  qed"in_rsch_asig";
   15.19  
   15.20  goal Abschannel.thy "srch_ioa = \
   15.21  \   (srch_asig, {{|}}, srch_trans,srch_wfair,srch_sfair)";
   15.22 -by (simp_tac (!simpset addsimps [srch_asig_def,srch_trans_def, asig_of_def, trans_of_def,
   15.23 +by (simp_tac (simpset() addsimps [srch_asig_def,srch_trans_def, asig_of_def, trans_of_def,
   15.24                wfair_of_def, sfair_of_def,srch_wfair_def,srch_sfair_def]) 1);
   15.25 -by(simp_tac (!simpset addsimps unfold_renaming) 1);
   15.26 +by(simp_tac (simpset() addsimps unfold_renaming) 1);
   15.27  qed"srch_ioa_thm";
   15.28  
   15.29  goal Abschannel.thy "rsch_ioa = \
   15.30  \    (rsch_asig, {{|}}, rsch_trans,rsch_wfair,rsch_sfair)";
   15.31 -by (simp_tac (!simpset addsimps [rsch_asig_def,rsch_trans_def, asig_of_def, trans_of_def,
   15.32 +by (simp_tac (simpset() addsimps [rsch_asig_def,rsch_trans_def, asig_of_def, trans_of_def,
   15.33                wfair_of_def, sfair_of_def,rsch_wfair_def,rsch_sfair_def]) 1);
   15.34 -by(simp_tac (!simpset addsimps unfold_renaming) 1);
   15.35 +by(simp_tac (simpset() addsimps unfold_renaming) 1);
   15.36  qed"rsch_ioa_thm";
   15.37  
    16.1 --- a/src/HOLCF/IOA/NTP/Correctness.ML	Mon Nov 03 12:36:48 1997 +0100
    16.2 +++ b/src/HOLCF/IOA/NTP/Correctness.ML	Mon Nov 03 14:06:27 1997 +0100
    16.3 @@ -15,11 +15,11 @@
    16.4  val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def,
    16.5                    Abschannel.srch_asig_def,Abschannel.rsch_asig_def];
    16.6  
    16.7 -(* Two simpsets: - !simpset is basic, ss' unfolds hom_ioas *)
    16.8 +(* Two simpsets: - simpset() is basic, ss' unfolds hom_ioas *)
    16.9  
   16.10  Delsimps [split_paired_All];
   16.11  
   16.12 -val ss' = (!simpset addsimps hom_ioas);
   16.13 +val ss' = (simpset() addsimps hom_ioas);
   16.14  
   16.15  
   16.16  (* A lemma about restricting the action signature of the implementation
   16.17 @@ -38,22 +38,22 @@
   16.18  \   | C_m_r => False          \
   16.19  \   | C_r_s => False          \
   16.20  \   | C_r_r(m) => False)";
   16.21 - by (simp_tac (!simpset addsimps ([externals_def, restrict_def,
   16.22 + by (simp_tac (simpset() addsimps ([externals_def, restrict_def,
   16.23                              restrict_asig_def, Spec.sig_def]
   16.24                              @asig_projections)) 1);
   16.25  
   16.26    by (Action.action.induct_tac "a" 1);
   16.27 -  by (ALLGOALS(simp_tac (!simpset addsimps [actions_def]@asig_projections)));
   16.28 +  by (ALLGOALS(simp_tac (simpset() addsimps [actions_def]@asig_projections)));
   16.29   (* 2 *)
   16.30 -  by (simp_tac (!simpset addsimps impl_ioas) 1);
   16.31 -  by (simp_tac (!simpset addsimps impl_asigs) 1);
   16.32 -  by (simp_tac (!simpset addsimps 
   16.33 +  by (simp_tac (simpset() addsimps impl_ioas) 1);
   16.34 +  by (simp_tac (simpset() addsimps impl_asigs) 1);
   16.35 +  by (simp_tac (simpset() addsimps 
   16.36               [asig_of_par, asig_comp_def]@asig_projections) 1);
   16.37    by (simp_tac rename_ss 1); 
   16.38   (* 1 *)
   16.39 -  by (simp_tac (!simpset addsimps impl_ioas) 1);
   16.40 -  by (simp_tac (!simpset addsimps impl_asigs) 1);
   16.41 -  by (simp_tac (!simpset addsimps 
   16.42 +  by (simp_tac (simpset() addsimps impl_ioas) 1);
   16.43 +  by (simp_tac (simpset() addsimps impl_asigs) 1);
   16.44 +  by (simp_tac (simpset() addsimps 
   16.45               [asig_of_par, asig_comp_def]@asig_projections) 1);
   16.46  qed "externals_lemma"; 
   16.47  
   16.48 @@ -66,18 +66,18 @@
   16.49  (* Proof of correctness *)
   16.50  goalw Correctness.thy [Spec.ioa_def, is_weak_ref_map_def]
   16.51    "is_weak_ref_map hom (restrict impl_ioa (externals spec_sig)) spec_ioa";
   16.52 -by (simp_tac (!simpset addsimps 
   16.53 +by (simp_tac (simpset() addsimps 
   16.54      [Correctness.hom_def, cancel_restrict, externals_lemma]) 1);
   16.55  by (rtac conjI 1);
   16.56  by (simp_tac ss' 1);
   16.57 -by (asm_simp_tac (!simpset addsimps sels) 1);
   16.58 +by (asm_simp_tac (simpset() addsimps sels) 1);
   16.59  by (REPEAT(rtac allI 1));
   16.60  by (rtac imp_conj_lemma 1);   (* from lemmas.ML *)
   16.61  
   16.62  by (Action.action.induct_tac "a"  1);
   16.63  by (asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);
   16.64  by (forward_tac [inv4] 1);
   16.65 -by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
   16.66 +by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
   16.67  by (simp_tac ss' 1);
   16.68  by (simp_tac ss' 1);
   16.69  by (simp_tac ss' 1);
   16.70 @@ -91,7 +91,7 @@
   16.71  by (forward_tac [inv2] 1);
   16.72  by (etac disjE 1);
   16.73  by (Asm_simp_tac 1);
   16.74 -by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
   16.75 +by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
   16.76  
   16.77  by (asm_simp_tac ss' 1);
   16.78  by (forward_tac [inv2] 1);
   16.79 @@ -101,14 +101,14 @@
   16.80  by (case_tac "sq(sen(s))=[]" 1);
   16.81  
   16.82  by (asm_full_simp_tac ss' 1);
   16.83 -by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
   16.84 +by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1);
   16.85  
   16.86  by (case_tac "m = hd(sq(sen(s)))" 1);
   16.87  
   16.88 -by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
   16.89 +by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
   16.90  
   16.91  by (Asm_full_simp_tac 1);
   16.92 -by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
   16.93 +by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1);
   16.94  
   16.95  by (Asm_full_simp_tac 1);
   16.96  qed"ntp_correct";
    17.1 --- a/src/HOLCF/IOA/NTP/Impl.ML	Mon Nov 03 12:36:48 1997 +0100
    17.2 +++ b/src/HOLCF/IOA/NTP/Impl.ML	Mon Nov 03 14:06:27 1997 +0100
    17.3 @@ -33,7 +33,7 @@
    17.4  \  fst(snd(x)) = rec(x)       & \
    17.5  \  fst(snd(snd(x))) = srch(x) & \
    17.6  \  snd(snd(snd(x))) = rsch(x)";
    17.7 -by(simp_tac (!simpset addsimps
    17.8 +by(simp_tac (simpset() addsimps
    17.9               [sen_def,rec_def,srch_def,rsch_def]) 1);
   17.10  Addsimps [result()];
   17.11  
   17.12 @@ -51,12 +51,12 @@
   17.13  (* Three Simp_sets in different sizes 
   17.14  ----------------------------------------------
   17.15  
   17.16 -1) !simpset does not unfold the transition relations 
   17.17 +1) simpset() does not unfold the transition relations 
   17.18  2) ss unfolds transition relations 
   17.19  3) renname_ss unfolds transitions and the abstract channel *)
   17.20  
   17.21  
   17.22 -val ss = (!simpset addcongs [if_weak_cong]
   17.23 +val ss = (simpset() addcongs [if_weak_cong]
   17.24                     addsimps transitions);     
   17.25  val rename_ss = (ss addsimps unfold_renaming);
   17.26  
   17.27 @@ -73,18 +73,18 @@
   17.28  
   17.29  goalw Impl.thy impl_ioas "invariant impl_ioa inv1";
   17.30  by (rtac invariantI 1);
   17.31 -by(asm_full_simp_tac (!simpset
   17.32 +by(asm_full_simp_tac (simpset()
   17.33     addsimps [inv1_def, hdr_sum_def, Sender.srcvd_def,
   17.34               Sender.ssent_def, Receiver.rsent_def,Receiver.rrcvd_def]) 1);
   17.35  
   17.36 -by(simp_tac (!simpset delsimps [trans_of_par4]
   17.37 +by(simp_tac (simpset() delsimps [trans_of_par4]
   17.38                  addsimps [fork_lemma,inv1_def]) 1);
   17.39  
   17.40  (* Split proof in two *)
   17.41  by (rtac conjI 1); 
   17.42  
   17.43  (* First half *)
   17.44 -by(asm_full_simp_tac (!simpset addsimps [Impl.inv1_def]) 1);
   17.45 +by(asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]) 1);
   17.46  by (rtac Action.action.induct 1);
   17.47  
   17.48  by (EVERY1[tac, tac, tac, tac]);
   17.49 @@ -101,7 +101,7 @@
   17.50  
   17.51  
   17.52  (* Now the other half *)
   17.53 -by(asm_full_simp_tac (!simpset addsimps [Impl.inv1_def]) 1);
   17.54 +by(asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]) 1);
   17.55  by (rtac Action.action.induct 1);
   17.56  by(EVERY1[tac, tac]);
   17.57  
   17.58 @@ -110,7 +110,7 @@
   17.59  by (tac_ren 1);
   17.60  by (rtac impI 1);
   17.61  by (REPEAT (etac conjE 1));
   17.62 -by (asm_simp_tac (!simpset addsimps [hdr_sum_def, Multiset.count_def,
   17.63 +by (asm_simp_tac (simpset() addsimps [hdr_sum_def, Multiset.count_def,
   17.64                                 Multiset.countm_nonempty_def]
   17.65                       setloop (split_tac [expand_if])) 1);
   17.66  (* detour 2 *)
   17.67 @@ -118,7 +118,7 @@
   17.68  by (tac_ren 1);
   17.69  by (rtac impI 1);
   17.70  by (REPEAT (etac conjE 1));
   17.71 -by (asm_full_simp_tac (!simpset addsimps [Impl.hdr_sum_def, 
   17.72 +by (asm_full_simp_tac (simpset() addsimps [Impl.hdr_sum_def, 
   17.73                                           Multiset.count_def,
   17.74                                           Multiset.countm_nonempty_def,
   17.75                                           Multiset.delm_nonempty_def,
   17.76 @@ -139,10 +139,10 @@
   17.77  
   17.78  by (rtac (countm_done_delm RS mp RS sym) 1);
   17.79  by (rtac refl 1);
   17.80 -by (asm_simp_tac (!simpset addsimps [Multiset.count_def]) 1);
   17.81 +by (asm_simp_tac (simpset() addsimps [Multiset.count_def]) 1);
   17.82  
   17.83  by (rtac impI 1);
   17.84 -by (asm_full_simp_tac (!simpset addsimps [neg_flip]) 1);
   17.85 +by (asm_full_simp_tac (simpset() addsimps [neg_flip]) 1);
   17.86  by (hyp_subst_tac 1);
   17.87  by (rtac countm_spurious_delm 1);
   17.88  by (Simp_tac 1);
   17.89 @@ -159,12 +159,12 @@
   17.90  
   17.91    by (rtac invariantI1 1); 
   17.92    (* Base case *)
   17.93 -  by (asm_full_simp_tac (!simpset addsimps (inv2_def ::
   17.94 +  by (asm_full_simp_tac (simpset() addsimps (inv2_def ::
   17.95                            (receiver_projections 
   17.96                             @ sender_projections @ impl_ioas)))
   17.97        1);
   17.98  
   17.99 -  by (asm_simp_tac (!simpset addsimps impl_ioas) 1);
  17.100 +  by (asm_simp_tac (simpset() addsimps impl_ioas) 1);
  17.101    by (Action.action.induct_tac "a" 1);
  17.102  
  17.103    (* 10 cases. First 4 are simple, since state doesn't change *)
  17.104 @@ -183,14 +183,14 @@
  17.105    by (forward_tac [rewrite_rule [Impl.inv1_def]
  17.106                                  (inv1 RS invariantE) RS conjunct1] 1);
  17.107    by (tac2 1);
  17.108 -  by (fast_tac (!claset addDs [add_leD1,leD]) 1);
  17.109 +  by (fast_tac (claset() addDs [add_leD1,leD]) 1);
  17.110  
  17.111    (* 3 *)
  17.112    by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1);
  17.113  
  17.114    by (tac2 1);
  17.115    by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]);
  17.116 -  by (fast_tac (!claset addDs [add_leD1,leD]) 1);
  17.117 +  by (fast_tac (claset() addDs [add_leD1,leD]) 1);
  17.118  
  17.119    (* 2 *)
  17.120    by (tac2 1);
  17.121 @@ -223,11 +223,11 @@
  17.122  
  17.123    by (rtac invariantI 1); 
  17.124    (* Base case *)
  17.125 -  by (asm_full_simp_tac (!simpset addsimps 
  17.126 +  by (asm_full_simp_tac (simpset() addsimps 
  17.127                      (Impl.inv3_def :: (receiver_projections 
  17.128                                         @ sender_projections @ impl_ioas))) 1);
  17.129  
  17.130 -  by (asm_simp_tac (!simpset addsimps impl_ioas) 1);
  17.131 +  by (asm_simp_tac (simpset() addsimps impl_ioas) 1);
  17.132    by (Action.action.induct_tac "a" 1);
  17.133  
  17.134  val tac3 = asm_full_simp_tac (ss addsimps [inv3_def] 
  17.135 @@ -254,7 +254,7 @@
  17.136  
  17.137    (* 2 *)
  17.138    by (asm_full_simp_tac ss 1);
  17.139 -  by (simp_tac (!simpset addsimps [inv3_def]) 1);
  17.140 +  by (simp_tac (simpset() addsimps [inv3_def]) 1);
  17.141    by (strip_tac  1 THEN REPEAT (etac conjE 1));
  17.142    by (rtac (imp_or_lem RS iffD2) 1);
  17.143    by (rtac impI 1);
  17.144 @@ -265,7 +265,7 @@
  17.145                      ("k","count (rsent(rec s)) (sbit(sen s))")] le_trans 1);
  17.146    by (forward_tac [rewrite_rule [inv1_def]
  17.147                                  (inv1 RS invariantE) RS conjunct2] 1);
  17.148 -  by (asm_full_simp_tac (!simpset addsimps
  17.149 +  by (asm_full_simp_tac (simpset() addsimps
  17.150                           [hdr_sum_def, Multiset.count_def]) 1);
  17.151    by (rtac (less_eq_add_cong RS mp RS mp) 1);
  17.152    by (rtac countm_props 1);
  17.153 @@ -298,11 +298,11 @@
  17.154  
  17.155    by (rtac invariantI 1); 
  17.156    (* Base case *)
  17.157 -  by (asm_full_simp_tac (!simpset addsimps 
  17.158 +  by (asm_full_simp_tac (simpset() addsimps 
  17.159                      (Impl.inv4_def :: (receiver_projections 
  17.160                                         @ sender_projections @ impl_ioas))) 1);
  17.161  
  17.162 -  by (asm_simp_tac (!simpset addsimps impl_ioas) 1);
  17.163 +  by (asm_simp_tac (simpset() addsimps impl_ioas) 1);
  17.164    by (Action.action.induct_tac "a" 1);
  17.165  
  17.166  val tac4 =  asm_full_simp_tac (ss addsimps [inv4_def]
    18.1 --- a/src/HOLCF/IOA/NTP/Lemmas.ML	Mon Nov 03 12:36:48 1997 +0100
    18.2 +++ b/src/HOLCF/IOA/NTP/Lemmas.ML	Mon Nov 03 14:06:27 1997 +0100
    18.3 @@ -10,7 +10,7 @@
    18.4  
    18.5  (* Logic *)
    18.6  val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    18.7 -  by(fast_tac (!claset addDs prems) 1);
    18.8 +  by(fast_tac (claset() addDs prems) 1);
    18.9  qed "imp_conj_lemma";
   18.10  
   18.11  goal HOL.thy "(P --> (? x. Q(x))) = (? x. P --> Q(x))";
   18.12 @@ -113,8 +113,8 @@
   18.13  goal Arith.thy "(A::nat) <= B --> C <= D --> A + C <= B + D";
   18.14    by (rtac impI 1);
   18.15    by (rtac impI 1);
   18.16 -  by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
   18.17 -  by (safe_tac (!claset));
   18.18 +  by (asm_full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
   18.19 +  by (safe_tac (claset()));
   18.20    by (rtac (less_add_cong RS mp RS mp) 1);
   18.21    by (assume_tac 1);
   18.22    by (assume_tac 1);
   18.23 @@ -131,7 +131,7 @@
   18.24    by (dtac (less_eq_add_cong RS mp) 1);
   18.25    by (cut_facts_tac [le_refl] 1);
   18.26    by (dres_inst_tac [("P","x<=x")] mp 1);by (assume_tac 1);
   18.27 -  by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1);
   18.28 +  by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
   18.29    by (rtac impI 1);
   18.30    by (etac le_trans 1);
   18.31    by (assume_tac 1);
   18.32 @@ -147,10 +147,10 @@
   18.33  
   18.34  goal Arith.thy "Suc(x) <= y --> (? z. y = Suc(z))";
   18.35    by (rtac impI 1);
   18.36 -  by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
   18.37 -  by (safe_tac (!claset));
   18.38 +  by (asm_full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
   18.39 +  by (safe_tac (claset()));
   18.40    by (Fast_tac 2);
   18.41 -  by (asm_simp_tac (!simpset addsimps [suc_not_zero]) 1);
   18.42 +  by (asm_simp_tac (simpset() addsimps [suc_not_zero]) 1);
   18.43  qed "suc_leq_suc";
   18.44  
   18.45  goal Arith.thy "~0<n --> n = 0";
   18.46 @@ -160,8 +160,8 @@
   18.47  
   18.48  goal Arith.thy "x < Suc(y) --> x<=y";
   18.49    by (nat_ind_tac "n" 1);
   18.50 -  by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   18.51 -  by (safe_tac (!claset));
   18.52 +  by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
   18.53 +  by (safe_tac (claset()));
   18.54    by (etac less_imp_le 1);
   18.55  qed "less_suc_imp_leq";
   18.56  
   18.57 @@ -187,12 +187,12 @@
   18.58  goal Arith.thy "((x::nat) = y + z) --> (y <= x)";
   18.59    by (nat_ind_tac "y" 1);
   18.60    by (Simp_tac 1);
   18.61 -  by (simp_tac (!simpset addsimps [le_refl RS (leq_add_leq RS mp)]) 1);
   18.62 +  by (simp_tac (simpset() addsimps [le_refl RS (leq_add_leq RS mp)]) 1);
   18.63  qed "plus_leq_lem";
   18.64  
   18.65  (* Lists *)
   18.66  
   18.67 -val list_ss = simpset_of "List";
   18.68 +val list_ss = simpset_of List.thy;
   18.69  
   18.70  goal List.thy "(xs @ (y#ys)) ~= []";
   18.71    by (list.induct_tac "xs" 1);
    19.1 --- a/src/HOLCF/IOA/NTP/Multiset.ML	Mon Nov 03 12:36:48 1997 +0100
    19.2 +++ b/src/HOLCF/IOA/NTP/Multiset.ML	Mon Nov 03 14:06:27 1997 +0100
    19.3 @@ -14,44 +14,44 @@
    19.4  
    19.5  goal Multiset.thy 
    19.6       "count (addm M x) y = (if y=x then Suc(count M y) else count M y)";
    19.7 -  by (asm_simp_tac (!simpset addsimps 
    19.8 +  by (asm_simp_tac (simpset() addsimps 
    19.9                      [Multiset.count_def,Multiset.countm_nonempty_def]
   19.10                      setloop (split_tac [expand_if])) 1);
   19.11  qed "count_addm_simp";
   19.12  
   19.13  goal Multiset.thy "count M y <= count (addm M x) y";
   19.14 -  by (simp_tac (!simpset addsimps [count_addm_simp]
   19.15 +  by (simp_tac (simpset() addsimps [count_addm_simp]
   19.16                           setloop (split_tac [expand_if])) 1);
   19.17  qed "count_leq_addm";
   19.18  
   19.19  goalw Multiset.thy [Multiset.count_def] 
   19.20       "count (delm M x) y = (if y=x then pred(count M y) else count M y)";
   19.21    by (res_inst_tac [("M","M")] Multiset.induction 1);
   19.22 -  by (asm_simp_tac (!simpset 
   19.23 +  by (asm_simp_tac (simpset() 
   19.24                     addsimps [Multiset.delm_empty_def,Multiset.countm_empty_def]
   19.25                     setloop (split_tac [expand_if])) 1);
   19.26 -  by (asm_full_simp_tac (!simpset 
   19.27 +  by (asm_full_simp_tac (simpset() 
   19.28                           addsimps [Multiset.delm_nonempty_def,
   19.29                                     Multiset.countm_nonempty_def]
   19.30                           setloop (split_tac [expand_if])) 1);
   19.31 -  by (safe_tac (!claset));
   19.32 +  by (safe_tac (claset()));
   19.33    by (Asm_full_simp_tac 1);
   19.34  qed "count_delm_simp";
   19.35  
   19.36  goal Multiset.thy "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)";
   19.37    by (res_inst_tac [("M","M")] Multiset.induction 1);
   19.38 -  by (simp_tac (!simpset addsimps [Multiset.countm_empty_def]) 1);
   19.39 -  by (simp_tac (!simpset addsimps[Multiset.countm_nonempty_def]) 1);
   19.40 +  by (simp_tac (simpset() addsimps [Multiset.countm_empty_def]) 1);
   19.41 +  by (simp_tac (simpset() addsimps[Multiset.countm_nonempty_def]) 1);
   19.42    by (etac (less_eq_add_cong RS mp RS mp) 1);
   19.43 -  by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]
   19.44 +  by (asm_full_simp_tac (simpset() addsimps [le_eq_less_or_eq]
   19.45                                    setloop (split_tac [expand_if])) 1);
   19.46  qed "countm_props";
   19.47  
   19.48  goal Multiset.thy "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P";
   19.49    by (res_inst_tac [("M","M")] Multiset.induction 1);
   19.50 -  by (simp_tac (!simpset addsimps [Multiset.delm_empty_def,
   19.51 +  by (simp_tac (simpset() addsimps [Multiset.delm_empty_def,
   19.52                                     Multiset.countm_empty_def]) 1);
   19.53 -  by (asm_simp_tac (!simpset addsimps[Multiset.countm_nonempty_def,
   19.54 +  by (asm_simp_tac (simpset() addsimps[Multiset.countm_nonempty_def,
   19.55                                        Multiset.delm_nonempty_def]
   19.56                               setloop (split_tac [expand_if])) 1);
   19.57  qed "countm_spurious_delm";
   19.58 @@ -59,10 +59,10 @@
   19.59  
   19.60  goal Multiset.thy "!!P. P(x) ==> 0<count M x --> 0<countm M P";
   19.61    by (res_inst_tac [("M","M")] Multiset.induction 1);
   19.62 -  by (simp_tac (!simpset addsimps 
   19.63 +  by (simp_tac (simpset() addsimps 
   19.64                            [Multiset.delm_empty_def,Multiset.count_def,
   19.65                             Multiset.countm_empty_def]) 1);
   19.66 -  by (asm_simp_tac (!simpset addsimps 
   19.67 +  by (asm_simp_tac (simpset() addsimps 
   19.68                         [Multiset.count_def,Multiset.delm_nonempty_def,
   19.69                          Multiset.countm_nonempty_def]
   19.70                      setloop (split_tac [expand_if])) 1);
   19.71 @@ -71,10 +71,10 @@
   19.72  goal Multiset.thy
   19.73     "!!P. P(x) ==> 0<count M x --> countm (delm M x) P = pred (countm M P)";
   19.74    by (res_inst_tac [("M","M")] Multiset.induction 1);
   19.75 -  by (simp_tac (!simpset addsimps 
   19.76 +  by (simp_tac (simpset() addsimps 
   19.77                            [Multiset.delm_empty_def,
   19.78                             Multiset.countm_empty_def]) 1);
   19.79 -  by (asm_simp_tac (!simpset addsimps 
   19.80 +  by (asm_simp_tac (simpset() addsimps 
   19.81                        [eq_sym_conv,count_addm_simp,Multiset.delm_nonempty_def,
   19.82                         Multiset.countm_nonempty_def,pos_count_imp_pos_countm,
   19.83                         suc_pred_id]
    20.1 --- a/src/HOLCF/IOA/NTP/Packet.ML	Mon Nov 03 12:36:48 1997 +0100
    20.2 +++ b/src/HOLCF/IOA/NTP/Packet.ML	Mon Nov 03 14:06:27 1997 +0100
    20.3 @@ -9,7 +9,7 @@
    20.4  
    20.5  (* Instantiation of a tautology? *)
    20.6  goal Packet.thy "!x. x = packet --> hdr(x) = hdr(packet)";
    20.7 - by (simp_tac (!simpset addsimps [Packet.hdr_def]) 1);
    20.8 + by (simp_tac (simpset() addsimps [Packet.hdr_def]) 1);
    20.9  qed "eq_packet_imp_eq_hdr"; 
   20.10  
   20.11  Addsimps [Packet.hdr_def,Packet.msg_def];
    21.1 --- a/src/HOLCF/IOA/NTP/Receiver.ML	Mon Nov 03 12:36:48 1997 +0100
    21.2 +++ b/src/HOLCF/IOA/NTP/Receiver.ML	Mon Nov 03 14:06:27 1997 +0100
    21.3 @@ -15,7 +15,7 @@
    21.4  \ C_m_r : actions(receiver_asig)          &   \
    21.5  \ C_r_s ~: actions(receiver_asig)         &   \
    21.6  \ C_r_r(m) : actions(receiver_asig)";
    21.7 -  by(simp_tac (!simpset addsimps (Receiver.receiver_asig_def :: actions_def :: 
    21.8 +  by(simp_tac (simpset() addsimps (Receiver.receiver_asig_def :: actions_def :: 
    21.9                                    asig_projections)) 1);
   21.10  qed "in_receiver_asig";
   21.11  
    22.1 --- a/src/HOLCF/IOA/NTP/Sender.ML	Mon Nov 03 12:36:48 1997 +0100
    22.2 +++ b/src/HOLCF/IOA/NTP/Sender.ML	Mon Nov 03 14:06:27 1997 +0100
    22.3 @@ -15,7 +15,7 @@
    22.4  \ C_m_r ~: actions(sender_asig)         &   \
    22.5  \ C_r_s : actions(sender_asig)          &   \
    22.6  \ C_r_r(m) ~: actions(sender_asig)";
    22.7 -by(simp_tac (!simpset addsimps 
    22.8 +by(simp_tac (simpset() addsimps 
    22.9               (Sender.sender_asig_def :: actions_def :: 
   22.10                asig_projections)) 1);
   22.11  qed "in_sender_asig";
    23.1 --- a/src/HOLCF/IOA/meta_theory/Asig.ML	Mon Nov 03 12:36:48 1997 +0100
    23.2 +++ b/src/HOLCF/IOA/meta_theory/Asig.ML	Mon Nov 03 14:06:27 1997 +0100
    23.3 @@ -14,40 +14,40 @@
    23.4   "(outputs    (a,b,c) = b)   & \
    23.5  \ (inputs     (a,b,c) = a) & \
    23.6  \ (internals  (a,b,c) = c)";
    23.7 -  by (simp_tac (!simpset addsimps asig_projections) 1);
    23.8 +  by (simp_tac (simpset() addsimps asig_projections) 1);
    23.9  qed "asig_triple_proj";
   23.10  
   23.11  goal thy "!!a.[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
   23.12 -by (asm_full_simp_tac (!simpset addsimps [externals_def,actions_def]) 1);
   23.13 +by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
   23.14  qed"int_and_ext_is_act";
   23.15  
   23.16  goal thy "!!a.[|a:externals(S)|] ==> a:actions(S)";
   23.17 -by (asm_full_simp_tac (!simpset addsimps [externals_def,actions_def]) 1);
   23.18 +by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
   23.19  qed"ext_is_act";
   23.20  
   23.21  goal thy "!!a.[|a:internals S|] ==> a:actions S";
   23.22 -by (asm_full_simp_tac (!simpset addsimps [asig_internals_def,actions_def]) 1);
   23.23 +by (asm_full_simp_tac (simpset() addsimps [asig_internals_def,actions_def]) 1);
   23.24  qed"int_is_act";
   23.25  
   23.26  goal thy "!!a.[|a:inputs S|] ==> a:actions S";
   23.27 -by (asm_full_simp_tac (!simpset addsimps [asig_inputs_def,actions_def]) 1);
   23.28 +by (asm_full_simp_tac (simpset() addsimps [asig_inputs_def,actions_def]) 1);
   23.29  qed"inp_is_act";
   23.30  
   23.31  goal thy "!!a.[|a:outputs S|] ==> a:actions S";
   23.32 -by (asm_full_simp_tac (!simpset addsimps [asig_outputs_def,actions_def]) 1);
   23.33 +by (asm_full_simp_tac (simpset() addsimps [asig_outputs_def,actions_def]) 1);
   23.34  qed"out_is_act";
   23.35  
   23.36  goal thy "(x: actions S & x : externals S) = (x: externals S)";
   23.37 -by (fast_tac (!claset addSIs [ext_is_act]) 1 );
   23.38 +by (fast_tac (claset() addSIs [ext_is_act]) 1 );
   23.39  qed"ext_and_act";
   23.40   
   23.41  goal thy "!!S. [|is_asig S;x: actions S|] ==> (x~:externals S) = (x: internals S)";
   23.42 -by (asm_full_simp_tac (!simpset addsimps [actions_def,is_asig_def,externals_def]) 1);
   23.43 +by (asm_full_simp_tac (simpset() addsimps [actions_def,is_asig_def,externals_def]) 1);
   23.44  by (best_tac (set_cs addEs [equalityCE]) 1);
   23.45  qed"not_ext_is_int";
   23.46  
   23.47  goal thy "!!S. is_asig S ==> (x~:externals S) = (x: internals S | x~:actions S)";
   23.48 -by (asm_full_simp_tac (!simpset addsimps [actions_def,is_asig_def,externals_def]) 1);
   23.49 +by (asm_full_simp_tac (simpset() addsimps [actions_def,is_asig_def,externals_def]) 1);
   23.50  by (best_tac (set_cs addEs [equalityCE]) 1);
   23.51  qed"not_ext_is_int_or_not_act";
   23.52  
    24.1 --- a/src/HOLCF/IOA/meta_theory/Automata.ML	Mon Nov 03 12:36:48 1997 +0100
    24.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Mon Nov 03 14:06:27 1997 +0100
    24.3 @@ -24,7 +24,7 @@
    24.4  \ ((trans_of (x,y,z,w,s)) = z)  & \
    24.5  \ ((wfair_of (x,y,z,w,s)) = w) & \
    24.6  \ ((sfair_of (x,y,z,w,s)) = s)";
    24.7 -  by (simp_tac (!simpset addsimps ioa_projections) 1);
    24.8 +  by (simp_tac (simpset() addsimps ioa_projections) 1);
    24.9  qed "ioa_triple_proj";
   24.10  
   24.11  goalw thy [is_trans_of_def,actions_def, is_asig_def]
   24.12 @@ -36,7 +36,7 @@
   24.13  
   24.14  goal thy
   24.15  "starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}";
   24.16 -  by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
   24.17 +  by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
   24.18  qed "starts_of_par";
   24.19  
   24.20  goal thy
   24.21 @@ -50,7 +50,7 @@
   24.22  \                  (snd(s),a,snd(t)):trans_of(B)     \                
   24.23  \                else snd(t) = snd(s))}";
   24.24  
   24.25 -by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
   24.26 +by(simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
   24.27  qed "trans_of_par";
   24.28  
   24.29  
   24.30 @@ -61,20 +61,20 @@
   24.31  
   24.32  goal thy 
   24.33  "actions(asig_comp a b) = actions(a) Un actions(b)";
   24.34 -  by (simp_tac (!simpset addsimps
   24.35 +  by (simp_tac (simpset() addsimps
   24.36                 ([actions_def,asig_comp_def]@asig_projections)) 1);
   24.37    by (fast_tac (set_cs addSIs [equalityI]) 1);
   24.38  qed "actions_asig_comp";
   24.39  
   24.40  
   24.41  goal thy "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)";
   24.42 -  by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
   24.43 +  by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
   24.44  qed "asig_of_par";
   24.45  
   24.46  
   24.47  goal thy "ext (A1||A2) =    \
   24.48  \  (ext A1) Un (ext A2)";
   24.49 -by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_of_par,asig_comp_def,
   24.50 +by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_of_par,asig_comp_def,
   24.51        asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1);
   24.52  by (rtac set_ext 1); 
   24.53  by (fast_tac set_cs 1);
   24.54 @@ -82,7 +82,7 @@
   24.55  
   24.56  goal thy "act (A1||A2) =    \
   24.57  \  (act A1) Un (act A2)";
   24.58 -by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def,
   24.59 +by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def,
   24.60        asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1);
   24.61  by (rtac set_ext 1); 
   24.62  by (fast_tac set_cs 1);
   24.63 @@ -90,19 +90,19 @@
   24.64  
   24.65  goal thy "inp (A1||A2) =\
   24.66  \         ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))";
   24.67 -by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def,
   24.68 +by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def,
   24.69        asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1);
   24.70  qed"inputs_of_par";
   24.71    
   24.72  goal thy "out (A1||A2) =\
   24.73  \         (out A1) Un (out A2)";
   24.74 -by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def,
   24.75 +by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def,
   24.76        asig_outputs_def,Un_def,set_diff_def]) 1);
   24.77  qed"outputs_of_par";
   24.78  
   24.79  goal thy "int (A1||A2) =\
   24.80  \         (int A1) Un (int A2)";
   24.81 -by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def,
   24.82 +by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def,
   24.83        asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1);
   24.84  qed"internals_of_par";
   24.85  
   24.86 @@ -111,7 +111,7 @@
   24.87  section "actions and compatibility"; 
   24.88  
   24.89  goal thy"compatible A B = compatible B A";
   24.90 -by (asm_full_simp_tac (!simpset addsimps [compatible_def,Int_commute]) 1);
   24.91 +by (asm_full_simp_tac (simpset() addsimps [compatible_def,Int_commute]) 1);
   24.92  by (Auto_tac());
   24.93  qed"compat_commute";
   24.94  
   24.95 @@ -170,10 +170,10 @@
   24.96  goalw thy [input_enabled_def] 
   24.97  "!!A. [| compatible A B; input_enabled A; input_enabled B|] \
   24.98  \     ==> input_enabled (A||B)";
   24.99 -by (asm_full_simp_tac (!simpset addsimps [inputs_of_par,trans_of_par]) 1);
  24.100 +by (asm_full_simp_tac (simpset() addsimps [inputs_of_par,trans_of_par]) 1);
  24.101  by (safe_tac set_cs);
  24.102 -by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
  24.103 -by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 2);
  24.104 +by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
  24.105 +by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 2);
  24.106  (* a: inp A *)
  24.107  by (case_tac "a:act B" 1);
  24.108  (* a:act B *)
  24.109 @@ -189,9 +189,9 @@
  24.110  be exE 1;
  24.111  be exE 1;
  24.112  by (res_inst_tac [("x","(s2,s2a)")] exI 1);
  24.113 -by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
  24.114 +by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
  24.115  (* a~: act B*)
  24.116 -by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
  24.117 +by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
  24.118  by (eres_inst_tac [("x","a")] allE 1);
  24.119  by (Asm_full_simp_tac 1);
  24.120  by (eres_inst_tac [("x","aa")] allE 1);
  24.121 @@ -204,7 +204,7 @@
  24.122  (* a:act A *)
  24.123  by (eres_inst_tac [("x","a")] allE 1);
  24.124  by (eres_inst_tac [("x","a")] allE 1);
  24.125 -by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
  24.126 +by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
  24.127  by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
  24.128  bd inpAAactB_is_inpBoroutB 1;
  24.129  back();
  24.130 @@ -218,9 +218,9 @@
  24.131  be exE 1;
  24.132  be exE 1;
  24.133  by (res_inst_tac [("x","(s2,s2a)")] exI 1);
  24.134 -by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
  24.135 +by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
  24.136  (* a~: act B*)
  24.137 -by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
  24.138 +by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
  24.139  by (eres_inst_tac [("x","a")] allE 1);
  24.140  by (Asm_full_simp_tac 1);
  24.141  by (eres_inst_tac [("x","a")] allE 1);
  24.142 @@ -268,25 +268,25 @@
  24.143  
  24.144  goal thy "starts_of(restrict ioa acts) = starts_of(ioa) &     \
  24.145  \         trans_of(restrict ioa acts) = trans_of(ioa)";
  24.146 -by (simp_tac (!simpset addsimps ([restrict_def]@ioa_projections)) 1);
  24.147 +by (simp_tac (simpset() addsimps ([restrict_def]@ioa_projections)) 1);
  24.148  qed "cancel_restrict_a";
  24.149  
  24.150  goal thy "reachable (restrict ioa acts) s = reachable ioa s";
  24.151  by (rtac iffI 1);
  24.152  by (etac reachable.induct 1);
  24.153 -by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a,reachable_0]) 1);
  24.154 +by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a,reachable_0]) 1);
  24.155  by (etac reachable_n 1);
  24.156 -by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
  24.157 +by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a]) 1);
  24.158  (* <--  *)
  24.159  by (etac reachable.induct 1);
  24.160  by (rtac reachable_0 1);
  24.161 -by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
  24.162 +by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a]) 1);
  24.163  by (etac reachable_n 1);
  24.164 -by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
  24.165 +by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a]) 1);
  24.166  qed "cancel_restrict_b";
  24.167  
  24.168  goal thy "act (restrict A acts) = act A";
  24.169 -by (simp_tac (!simpset addsimps [actions_def,asig_internals_def,
  24.170 +by (simp_tac (simpset() addsimps [actions_def,asig_internals_def,
  24.171          asig_outputs_def,asig_inputs_def,externals_def,asig_of_def,restrict_def,
  24.172          restrict_asig_def]) 1);
  24.173  auto();
  24.174 @@ -296,7 +296,7 @@
  24.175  \         trans_of(restrict ioa acts) = trans_of(ioa) & \
  24.176  \         reachable (restrict ioa acts) s = reachable ioa s & \
  24.177  \         act (restrict A acts) = act A";
  24.178 -  by (simp_tac (!simpset addsimps [cancel_restrict_a,cancel_restrict_b,acts_restrict]) 1);
  24.179 +  by (simp_tac (simpset() addsimps [cancel_restrict_a,cancel_restrict_b,acts_restrict]) 1);
  24.180  qed"cancel_restrict";
  24.181  
  24.182  (* ---------------------------------------------------------------------------------- *)
  24.183 @@ -306,14 +306,14 @@
  24.184  
  24.185  
  24.186  goal thy "!!f. s -a--(rename C f)-> t ==> (? x. Some(x) = f(a) & s -x--C-> t)";
  24.187 -by (asm_full_simp_tac (!simpset addsimps [Let_def,rename_def,trans_of_def]) 1);
  24.188 +by (asm_full_simp_tac (simpset() addsimps [Let_def,rename_def,trans_of_def]) 1);
  24.189  qed"trans_rename";
  24.190  
  24.191  
  24.192  goal thy "!!s.[| reachable (rename C g) s |] ==> reachable C s";
  24.193  by (etac reachable.induct 1);
  24.194  by (rtac reachable_0 1);
  24.195 -by (asm_full_simp_tac (!simpset addsimps [rename_def]@ioa_projections) 1);
  24.196 +by (asm_full_simp_tac (simpset() addsimps [rename_def]@ioa_projections) 1);
  24.197  by (dtac trans_rename 1);
  24.198  by (etac exE 1);
  24.199  by (etac conjE 1);
  24.200 @@ -330,45 +330,45 @@
  24.201  
  24.202  goal thy "!!A.[|(s,a,t):trans_of (A||B); a:act A|] \
  24.203  \             ==> (fst s,a,fst t):trans_of A";
  24.204 -by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
  24.205 +by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
  24.206  qed"trans_A_proj";
  24.207  
  24.208  goal thy "!!A.[|(s,a,t):trans_of (A||B); a:act B|] \
  24.209  \             ==> (snd s,a,snd t):trans_of B";
  24.210 -by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
  24.211 +by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
  24.212  qed"trans_B_proj";
  24.213  
  24.214  goal thy "!!A.[|(s,a,t):trans_of (A||B); a~:act A|]\
  24.215  \             ==> fst s = fst t";
  24.216 -by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
  24.217 +by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
  24.218  qed"trans_A_proj2";
  24.219  
  24.220  goal thy "!!A.[|(s,a,t):trans_of (A||B); a~:act B|]\
  24.221  \             ==> snd s = snd t";
  24.222 -by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
  24.223 +by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
  24.224  qed"trans_B_proj2";
  24.225  
  24.226  goal thy "!!A.(s,a,t):trans_of (A||B) \
  24.227  \              ==> a :act A | a :act B";
  24.228 -by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
  24.229 +by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
  24.230  qed"trans_AB_proj";
  24.231  
  24.232  goal thy "!!A. [|a:act A;a:act B;\
  24.233  \      (fst s,a,fst t):trans_of A;(snd s,a,snd t):trans_of B|]\
  24.234  \  ==> (s,a,t):trans_of (A||B)";
  24.235 -by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
  24.236 +by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
  24.237  qed"trans_AB";
  24.238  
  24.239  goal thy "!!A. [|a:act A;a~:act B;\
  24.240  \      (fst s,a,fst t):trans_of A;snd s=snd t|]\
  24.241  \  ==> (s,a,t):trans_of (A||B)";
  24.242 -by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
  24.243 +by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
  24.244  qed"trans_A_notB";
  24.245  
  24.246  goal thy "!!A. [|a~:act A;a:act B;\
  24.247  \      (snd s,a,snd t):trans_of B;fst s=fst t|]\
  24.248  \  ==> (s,a,t):trans_of (A||B)";
  24.249 -by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
  24.250 +by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
  24.251  qed"trans_notA_B";
  24.252  
  24.253  val trans_of_defs1 = [trans_AB,trans_A_notB,trans_notA_B];
  24.254 @@ -391,7 +391,7 @@
  24.255  \     (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)                      \
  24.256  \   else snd(snd(snd(t)))=snd(snd(snd(s)))))";
  24.257  
  24.258 -  by (simp_tac (!simpset addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@
  24.259 +  by (simp_tac (simpset() addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@
  24.260                              ioa_projections)
  24.261                    setloop (split_tac [expand_if])) 1);
  24.262  qed "trans_of_par4";
  24.263 @@ -404,17 +404,17 @@
  24.264  (* without assumptions on A and B because is_trans_of is also incorporated in ||def *)
  24.265  goalw thy [is_trans_of_def] 
  24.266  "is_trans_of (A||B)";
  24.267 -by (simp_tac (!simpset addsimps [actions_of_par,trans_of_par]) 1);
  24.268 +by (simp_tac (simpset() addsimps [actions_of_par,trans_of_par]) 1);
  24.269  qed"is_trans_of_par";
  24.270  
  24.271  goalw thy [is_trans_of_def] 
  24.272  "!!A. is_trans_of A ==> is_trans_of (restrict A acts)";
  24.273 -by (asm_simp_tac (!simpset addsimps [cancel_restrict,acts_restrict])1);
  24.274 +by (asm_simp_tac (simpset() addsimps [cancel_restrict,acts_restrict])1);
  24.275  qed"is_trans_of_restrict";
  24.276  
  24.277  goalw thy [is_trans_of_def,restrict_def,restrict_asig_def] 
  24.278  "!!A. is_trans_of A ==> is_trans_of (rename A f)";
  24.279 -by (asm_full_simp_tac (!simpset addsimps [actions_def,trans_of_def,
  24.280 +by (asm_full_simp_tac (simpset() addsimps [actions_def,trans_of_def,
  24.281      asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,
  24.282     asig_of_def,rename_def,rename_set_def]) 1);
  24.283  auto();
  24.284 @@ -422,10 +422,10 @@
  24.285  
  24.286  goal thy "!! A. [| is_asig_of A; is_asig_of B; compatible A B|]  \
  24.287  \         ==> is_asig_of (A||B)";
  24.288 -by (asm_full_simp_tac (!simpset addsimps [is_asig_of_def,asig_of_par,
  24.289 +by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,asig_of_par,
  24.290         asig_comp_def,compatible_def,asig_internals_def,asig_outputs_def,
  24.291       asig_inputs_def,actions_def,is_asig_def]) 1);
  24.292 -by (asm_full_simp_tac (!simpset addsimps [asig_of_def]) 1);
  24.293 +by (asm_full_simp_tac (simpset() addsimps [asig_of_def]) 1);
  24.294  auto();
  24.295  by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
  24.296  qed"is_asig_of_par";
  24.297 @@ -439,7 +439,7 @@
  24.298  qed"is_asig_of_restrict";
  24.299  
  24.300  goal thy "!! A. is_asig_of A ==> is_asig_of (rename A f)";
  24.301 -by (asm_full_simp_tac (!simpset addsimps [is_asig_of_def,
  24.302 +by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,
  24.303       rename_def,rename_set_def,asig_internals_def,asig_outputs_def,
  24.304       asig_inputs_def,actions_def,is_asig_def,asig_of_def]) 1);
  24.305  auto(); 
  24.306 @@ -464,7 +464,7 @@
  24.307  
  24.308  goalw thy [compatible_def]
  24.309  "!! A. [|compatible A B; compatible A C |]==> compatible A (B||C)";
  24.310 -by (asm_full_simp_tac (!simpset addsimps [internals_of_par, 
  24.311 +by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
  24.312     outputs_of_par,actions_of_par]) 1);
  24.313  auto();
  24.314  by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
  24.315 @@ -473,7 +473,7 @@
  24.316  (* FIX: better derive by previous one and compat_commute *)
  24.317  goalw thy [compatible_def]
  24.318  "!! A. [|compatible A C; compatible B C |]==> compatible (A||B) C";
  24.319 -by (asm_full_simp_tac (!simpset addsimps [internals_of_par, 
  24.320 +by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
  24.321     outputs_of_par,actions_of_par]) 1);
  24.322  auto();
  24.323  by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
  24.324 @@ -482,8 +482,8 @@
  24.325  goalw thy [compatible_def]
  24.326  "!! A. [| compatible A B; (ext B - S) Int ext A = {}|] \
  24.327  \     ==> compatible A (restrict B S)";
  24.328 -by (asm_full_simp_tac (!simpset addsimps [ioa_triple_proj,asig_triple_proj,
  24.329 +by (asm_full_simp_tac (simpset() addsimps [ioa_triple_proj,asig_triple_proj,
  24.330            externals_def,restrict_def,restrict_asig_def,actions_def]) 1);
  24.331 -by (auto_tac (!claset addEs [equalityCE],!simpset));
  24.332 +by (auto_tac (claset() addEs [equalityCE],simpset()));
  24.333  qed"compatible_restrict";
  24.334   
  24.335 \ No newline at end of file
    25.1 --- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Mon Nov 03 12:36:48 1997 +0100
    25.2 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Mon Nov 03 14:06:27 1997 +0100
    25.3 @@ -21,15 +21,15 @@
    25.4  
    25.5  
    25.6  goal thy  "ProjA2`UU = UU";
    25.7 -by (simp_tac (!simpset addsimps [ProjA2_def]) 1);
    25.8 +by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
    25.9  qed"ProjA2_UU";
   25.10  
   25.11  goal thy  "ProjA2`nil = nil";
   25.12 -by (simp_tac (!simpset addsimps [ProjA2_def]) 1);
   25.13 +by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
   25.14  qed"ProjA2_nil";
   25.15  
   25.16  goal thy "ProjA2`((a,t)>>xs) = (a,fst t) >> ProjA2`xs";
   25.17 -by (simp_tac (!simpset addsimps [ProjA2_def]) 1);
   25.18 +by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
   25.19  qed"ProjA2_cons";
   25.20  
   25.21  
   25.22 @@ -39,15 +39,15 @@
   25.23  
   25.24  
   25.25  goal thy  "ProjB2`UU = UU";
   25.26 -by (simp_tac (!simpset addsimps [ProjB2_def]) 1);
   25.27 +by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
   25.28  qed"ProjB2_UU";
   25.29  
   25.30  goal thy  "ProjB2`nil = nil";
   25.31 -by (simp_tac (!simpset addsimps [ProjB2_def]) 1);
   25.32 +by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
   25.33  qed"ProjB2_nil";
   25.34  
   25.35  goal thy "ProjB2`((a,t)>>xs) = (a,snd t) >> ProjB2`xs";
   25.36 -by (simp_tac (!simpset addsimps [ProjB2_def]) 1);
   25.37 +by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
   25.38  qed"ProjB2_cons";
   25.39  
   25.40  
   25.41 @@ -58,11 +58,11 @@
   25.42  
   25.43  
   25.44  goal thy "Filter_ex2 sig`UU=UU";
   25.45 -by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1);
   25.46 +by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
   25.47  qed"Filter_ex2_UU";
   25.48  
   25.49  goal thy "Filter_ex2 sig`nil=nil";
   25.50 -by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1);
   25.51 +by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
   25.52  qed"Filter_ex2_nil";
   25.53  
   25.54  goal thy "Filter_ex2 sig`(at >> xs) =    \
   25.55 @@ -70,7 +70,7 @@
   25.56  \                 then at >> (Filter_ex2 sig`xs) \   
   25.57  \                 else        Filter_ex2 sig`xs)";
   25.58  
   25.59 -by (asm_full_simp_tac (!simpset addsimps [Filter_ex2_def]) 1);
   25.60 +by (asm_full_simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
   25.61  qed"Filter_ex2_cons";
   25.62  
   25.63  
   25.64 @@ -92,7 +92,7 @@
   25.65  by (rtac fix_eq2 1);
   25.66  by (rtac stutter2_def 1);
   25.67  by (rtac beta_cfun 1);
   25.68 -by (simp_tac (!simpset addsimps [flift1_def]) 1);
   25.69 +by (simp_tac (simpset() addsimps [flift1_def]) 1);
   25.70  qed"stutter2_unfold";
   25.71  
   25.72  goal thy "(stutter2 sig`UU) s=UU";
   25.73 @@ -110,7 +110,7 @@
   25.74  \                andalso (stutter2 sig`xs) (snd at))"; 
   25.75  br trans 1;
   25.76  by (stac stutter2_unfold 1);
   25.77 -by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def,If_and_if]) 1);
   25.78 +by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def,If_and_if]) 1);
   25.79  by (Simp_tac 1);
   25.80  qed"stutter2_cons";
   25.81  
   25.82 @@ -123,16 +123,16 @@
   25.83  (* ---------------------------------------------------------------- *)
   25.84  
   25.85  goal thy "stutter sig (s, UU)";
   25.86 -by (simp_tac (!simpset addsimps [stutter_def]) 1);
   25.87 +by (simp_tac (simpset() addsimps [stutter_def]) 1);
   25.88  qed"stutter_UU";
   25.89  
   25.90  goal thy "stutter sig (s, nil)";
   25.91 -by (simp_tac (!simpset addsimps [stutter_def]) 1);
   25.92 +by (simp_tac (simpset() addsimps [stutter_def]) 1);
   25.93  qed"stutter_nil";
   25.94  
   25.95  goal thy "stutter sig (s, (a,t)>>ex) = \
   25.96  \     ((a~:actions sig --> (s=t)) & stutter sig (t,ex))";
   25.97 -by (simp_tac (!simpset addsimps [stutter_def] 
   25.98 +by (simp_tac (simpset() addsimps [stutter_def] 
   25.99                         setloop (split_tac [expand_if]) ) 1);
  25.100  qed"stutter_cons";
  25.101  
  25.102 @@ -167,7 +167,7 @@
  25.103  (* main case *)
  25.104  ren "ss a t" 1;
  25.105  by (safe_tac set_cs);
  25.106 -by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2
  25.107 +by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2
  25.108                         setloop (split_tac [expand_if])) 1));
  25.109  qed"lemma_1_1a";
  25.110  
  25.111 @@ -183,7 +183,7 @@
  25.112  by (pair_induct_tac "xs" [stutter_def,is_exec_frag_def] 1);
  25.113  (* main case *)
  25.114  by (safe_tac set_cs);
  25.115 -by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2
  25.116 +by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2
  25.117                   setloop (split_tac [expand_if])) 1));
  25.118  qed"lemma_1_1b";
  25.119  
  25.120 @@ -198,7 +198,7 @@
  25.121  by (pair_induct_tac "xs" [Forall_def,sforall_def,is_exec_frag_def] 1);
  25.122  (* main case *)
  25.123  by (safe_tac set_cs);
  25.124 -by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 @ 
  25.125 +by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2 @ 
  25.126                                  [actions_asig_comp,asig_of_par]) 1));
  25.127  qed"lemma_1_1c";
  25.128  
  25.129 @@ -220,14 +220,14 @@
  25.130  (* main case *)
  25.131  by (rtac allI 1); 
  25.132  ren "ss a t s" 1;
  25.133 -by (asm_full_simp_tac (!simpset addsimps trans_of_defs1 @ [actions_asig_comp,asig_of_par]
  25.134 +by (asm_full_simp_tac (simpset() addsimps trans_of_defs1 @ [actions_asig_comp,asig_of_par]
  25.135                 setloop (split_tac [expand_if])) 1);
  25.136  by (safe_tac set_cs);
  25.137  (* problem with asm_full_simp_tac: (fst s) = (fst t) is too high in assumption order ! *)
  25.138  by (rotate_tac ~4 1);
  25.139 -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  25.140 +by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
  25.141  by (rotate_tac ~4 1);
  25.142 -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  25.143 +by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
  25.144  qed"lemma_1_2";
  25.145  
  25.146  
  25.147 @@ -244,17 +244,17 @@
  25.148  \ stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &\
  25.149  \ Forall (%x. fst x:act (A||B)) (snd ex))";
  25.150  
  25.151 -by (simp_tac (!simpset addsimps [executions_def,ProjB_def,
  25.152 +by (simp_tac (simpset() addsimps [executions_def,ProjB_def,
  25.153                                   Filter_ex_def,ProjA_def,starts_of_par]) 1);
  25.154  by (pair_tac "ex" 1);
  25.155  by (rtac iffI 1);
  25.156  (* ==>  *)
  25.157  by (REPEAT (etac conjE 1));
  25.158 -by (asm_full_simp_tac (!simpset addsimps [lemma_1_1a RS spec RS mp,
  25.159 +by (asm_full_simp_tac (simpset() addsimps [lemma_1_1a RS spec RS mp,
  25.160                 lemma_1_1b RS spec RS mp,lemma_1_1c RS spec RS mp]) 1);
  25.161  (* <==  *)
  25.162  by (REPEAT (etac conjE 1));
  25.163 -by (asm_full_simp_tac (!simpset addsimps [lemma_1_2 RS spec RS mp]) 1);
  25.164 +by (asm_full_simp_tac (simpset() addsimps [lemma_1_2 RS spec RS mp]) 1);
  25.165  qed"compositionality_ex";
  25.166  
  25.167  
  25.168 @@ -267,9 +267,9 @@
  25.169  
  25.170  "Execs (A||B) = par_execs (Execs A) (Execs B)";
  25.171  
  25.172 -by (asm_full_simp_tac (!simpset addsimps [asig_of_par]) 1);
  25.173 +by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
  25.174  br set_ext 1;
  25.175 -by (asm_full_simp_tac (!simpset addsimps [compositionality_ex,actions_of_par]) 1);
  25.176 +by (asm_full_simp_tac (simpset() addsimps [compositionality_ex,actions_of_par]) 1);
  25.177  qed"compositionality_ex_modules";
  25.178  
  25.179  
    26.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Mon Nov 03 12:36:48 1997 +0100
    26.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Mon Nov 03 14:06:27 1997 +0100
    26.3 @@ -71,8 +71,8 @@
    26.4  \       (x,snd a,t) >> (mkex2 A B`sch`(TL`exA)`exB) (snd a) t";
    26.5  by (rtac trans 1);
    26.6  by (stac mkex2_unfold 1);
    26.7 -by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
    26.8 -by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
    26.9 +by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
   26.10 +by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
   26.11  qed"mkex2_cons_1";
   26.12  
   26.13  goal thy "!!x.[| x~:act A; x:act B; HD`exB=Def b|] \
   26.14 @@ -80,8 +80,8 @@
   26.15  \       (x,s,snd b) >> (mkex2 A B`sch`exA`(TL`exB)) s (snd b)";
   26.16  by (rtac trans 1);
   26.17  by (stac mkex2_unfold 1);
   26.18 -by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
   26.19 -by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
   26.20 +by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
   26.21 +by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
   26.22  qed"mkex2_cons_2";
   26.23  
   26.24  goal thy "!!x.[| x:act A; x:act B; HD`exA=Def a;HD`exB=Def b|] \
   26.25 @@ -90,8 +90,8 @@
   26.26  \           (mkex2 A B`sch`(TL`exA)`(TL`exB)) (snd a) (snd b)";
   26.27  by (rtac trans 1);
   26.28  by (stac mkex2_unfold 1);
   26.29 -by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
   26.30 -by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
   26.31 +by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
   26.32 +by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
   26.33  qed"mkex2_cons_3";
   26.34  
   26.35  Addsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3];
   26.36 @@ -102,17 +102,17 @@
   26.37  (* ---------------------------------------------------------------- *)
   26.38  
   26.39  goal thy "mkex A B UU  (s,exA) (t,exB) = ((s,t),UU)";
   26.40 -by (simp_tac (!simpset addsimps [mkex_def]) 1);
   26.41 +by (simp_tac (simpset() addsimps [mkex_def]) 1);
   26.42  qed"mkex_UU";
   26.43  
   26.44  goal thy "mkex A B nil (s,exA) (t,exB) = ((s,t),nil)";
   26.45 -by (simp_tac (!simpset addsimps [mkex_def]) 1);
   26.46 +by (simp_tac (simpset() addsimps [mkex_def]) 1);
   26.47  qed"mkex_nil";
   26.48  
   26.49  goal thy "!!x.[| x:act A; x~:act B |] \
   26.50  \   ==> mkex A B (x>>sch) (s,a>>exA) (t,exB)  =  \
   26.51  \       ((s,t), (x,snd a,t) >> snd (mkex A B sch (snd a,exA) (t,exB)))";
   26.52 -by (simp_tac (!simpset addsimps [mkex_def] 
   26.53 +by (simp_tac (simpset() addsimps [mkex_def] 
   26.54                         setloop (split_tac [expand_if]) ) 1);
   26.55  by (cut_inst_tac [("exA","a>>exA")] mkex2_cons_1 1);
   26.56  by (Auto_tac());
   26.57 @@ -121,7 +121,7 @@
   26.58  goal thy "!!x.[| x~:act A; x:act B |] \
   26.59  \   ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) =  \ 
   26.60  \       ((s,t), (x,s,snd b) >> snd (mkex A B sch (s,exA) (snd b,exB)))";
   26.61 -by (simp_tac (!simpset addsimps [mkex_def] 
   26.62 +by (simp_tac (simpset() addsimps [mkex_def] 
   26.63                         setloop (split_tac [expand_if]) ) 1);
   26.64  by (cut_inst_tac [("exB","b>>exB")] mkex2_cons_2 1);
   26.65  by (Auto_tac());
   26.66 @@ -130,7 +130,7 @@
   26.67  goal thy "!!x.[| x:act A; x:act B |]  \
   26.68  \   ==>  mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) = \
   26.69  \        ((s,t), (x,snd a,snd b) >> snd (mkex A B sch (snd a,exA) (snd b,exB)))";
   26.70 -by (simp_tac (!simpset addsimps [mkex_def] 
   26.71 +by (simp_tac (simpset() addsimps [mkex_def] 
   26.72                         setloop (split_tac [expand_if]) ) 1);
   26.73  by (cut_inst_tac [("exB","b>>exB"),("exA","a>>exA")] mkex2_cons_3 1);
   26.74  by (Auto_tac());
   26.75 @@ -162,7 +162,7 @@
   26.76     "filter_act`(Filter_ex2 (asig_of A)`xs)=\
   26.77  \   Filter (%a. a:act A)`(filter_act`xs)";
   26.78  
   26.79 -by (simp_tac (!simpset addsimps [MapFilter,o_def]) 1);
   26.80 +by (simp_tac (simpset() addsimps [MapFilter,o_def]) 1);
   26.81  qed"lemma_2_1a";
   26.82  
   26.83  
   26.84 @@ -192,7 +192,7 @@
   26.85  by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
   26.86  (* main case *)
   26.87  by (safe_tac set_cs);
   26.88 -by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 @ 
   26.89 +by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2 @ 
   26.90                                  [actions_asig_comp,asig_of_par]) 1));
   26.91  qed"sch_actions_in_AorB";
   26.92  
   26.93 @@ -216,7 +216,7 @@
   26.94  
   26.95  (* main case *) 
   26.96  (* splitting into 4 cases according to a:A, a:B *)
   26.97 -by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
   26.98 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
   26.99  by (safe_tac set_cs);
  26.100  
  26.101  (* Case y:A, y:B *)
  26.102 @@ -241,7 +241,7 @@
  26.103  by (Asm_full_simp_tac 1);
  26.104  
  26.105  (* Case y~:A, y~:B *)
  26.106 -by (asm_full_simp_tac (!simpset addsimps [asig_of_par,actions_asig_comp]) 1);
  26.107 +by (asm_full_simp_tac (simpset() addsimps [asig_of_par,actions_asig_comp]) 1);
  26.108  qed"Mapfst_mkex_is_sch";
  26.109  
  26.110  
  26.111 @@ -249,7 +249,7 @@
  26.112  
  26.113  fun mkex_induct_tac sch exA exB = 
  26.114      EVERY1[Seq_induct_tac sch [Filter_def,Forall_def,sforall_def,mkex_def,stutter_def], 
  26.115 -           asm_full_simp_tac (!simpset setloop split_tac [expand_if]),
  26.116 +           asm_full_simp_tac (simpset() setloop split_tac [expand_if]),
  26.117             SELECT_GOAL (safe_tac set_cs),
  26.118             Seq_case_simp_tac exA,
  26.119             Seq_case_simp_tac exB,
  26.120 @@ -258,7 +258,7 @@
  26.121             Asm_full_simp_tac,
  26.122             Seq_case_simp_tac exA,
  26.123             Asm_full_simp_tac,
  26.124 -           asm_full_simp_tac (!simpset addsimps [asig_of_par,actions_asig_comp])
  26.125 +           asm_full_simp_tac (simpset() addsimps [asig_of_par,actions_asig_comp])
  26.126            ];
  26.127  
  26.128  
  26.129 @@ -287,7 +287,7 @@
  26.130  \ ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))";
  26.131  
  26.132  by (cut_facts_tac [stutterA_mkex] 1);
  26.133 -by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjA_def,mkex_def]) 1);
  26.134 +by (asm_full_simp_tac (simpset() addsimps [stutter_def,ProjA_def,mkex_def]) 1);
  26.135  by (REPEAT (etac allE 1));
  26.136  by (dtac mp 1);
  26.137  by (assume_tac 2);
  26.138 @@ -318,7 +318,7 @@
  26.139  \ ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))";
  26.140  
  26.141  by (cut_facts_tac [stutterB_mkex] 1);
  26.142 -by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjB_def,mkex_def]) 1);
  26.143 +by (asm_full_simp_tac (simpset() addsimps [stutter_def,ProjB_def,mkex_def]) 1);
  26.144  by (REPEAT (etac allE 1));
  26.145  by (dtac mp 1);
  26.146  by (assume_tac 2);
  26.147 @@ -362,7 +362,7 @@
  26.148  goal thy "!! sch ex. \
  26.149  \ Filter (%a. a:act AB)`sch = filter_act`ex  \
  26.150  \ ==> ex = Zip`(Filter (%a. a:act AB)`sch)`(Map snd`ex)";
  26.151 -by (asm_full_simp_tac (!simpset addsimps [filter_act_def]) 1);
  26.152 +by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 1);
  26.153  by (rtac (Zip_Map_fst_snd RS sym) 1);
  26.154  qed"trick_against_eq_in_ass";
  26.155  
  26.156 @@ -377,15 +377,15 @@
  26.157  \ Filter (%a. a:act A)`sch = filter_act`(snd exA)  ;\
  26.158  \ Filter (%a. a:act B)`sch = filter_act`(snd exB) |]\
  26.159  \ ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA";
  26.160 -by (asm_full_simp_tac (!simpset addsimps [ProjA_def,Filter_ex_def]) 1);
  26.161 +by (asm_full_simp_tac (simpset() addsimps [ProjA_def,Filter_ex_def]) 1);
  26.162  by (pair_tac "exA" 1);
  26.163  by (pair_tac "exB" 1);
  26.164  by (rtac conjI 1);
  26.165 -by (simp_tac (!simpset addsimps [mkex_def]) 1);
  26.166 +by (simp_tac (simpset() addsimps [mkex_def]) 1);
  26.167  by (stac trick_against_eq_in_ass 1);
  26.168  back();
  26.169  by (assume_tac 1);
  26.170 -by (asm_full_simp_tac (!simpset addsimps [filter_mkex_is_exA_tmp]) 1);
  26.171 +by (asm_full_simp_tac (simpset() addsimps [filter_mkex_is_exA_tmp]) 1);
  26.172  qed"filter_mkex_is_exA";
  26.173   
  26.174  
  26.175 @@ -421,15 +421,15 @@
  26.176  \ Filter (%a. a:act A)`sch = filter_act`(snd exA)  ;\
  26.177  \ Filter (%a. a:act B)`sch = filter_act`(snd exB) |]\
  26.178  \ ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB";
  26.179 -by (asm_full_simp_tac (!simpset addsimps [ProjB_def,Filter_ex_def]) 1);
  26.180 +by (asm_full_simp_tac (simpset() addsimps [ProjB_def,Filter_ex_def]) 1);
  26.181  by (pair_tac "exA" 1);
  26.182  by (pair_tac "exB" 1);
  26.183  by (rtac conjI 1);
  26.184 -by (simp_tac (!simpset addsimps [mkex_def]) 1);
  26.185 +by (simp_tac (simpset() addsimps [mkex_def]) 1);
  26.186  by (stac trick_against_eq_in_ass 1);
  26.187  back();
  26.188  by (assume_tac 1);
  26.189 -by (asm_full_simp_tac (!simpset addsimps [filter_mkex_is_exB_tmp]) 1);
  26.190 +by (asm_full_simp_tac (simpset() addsimps [filter_mkex_is_exB_tmp]) 1);
  26.191  qed"filter_mkex_is_exB";
  26.192  
  26.193  (* --------------------------------------------------------------------- *)
  26.194 @@ -460,21 +460,21 @@
  26.195  \  Filter (%a. a:act B)`sch : schedules B &\
  26.196  \  Forall (%x. x:act (A||B)) sch)";
  26.197  
  26.198 -by (simp_tac (!simpset addsimps [schedules_def, has_schedule_def]) 1);
  26.199 +by (simp_tac (simpset() addsimps [schedules_def, has_schedule_def]) 1);
  26.200  by (safe_tac set_cs); 
  26.201  (* ==> *) 
  26.202  by (res_inst_tac [("x","Filter_ex (asig_of A) (ProjA ex)")] bexI 1);
  26.203 -by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 2);
  26.204 -by (simp_tac (!simpset addsimps [Filter_ex_def,ProjA_def,
  26.205 +by (asm_full_simp_tac (simpset() addsimps [compositionality_ex]) 2);
  26.206 +by (simp_tac (simpset() addsimps [Filter_ex_def,ProjA_def,
  26.207                                   lemma_2_1a,lemma_2_1b]) 1); 
  26.208  by (res_inst_tac [("x","Filter_ex (asig_of B) (ProjB ex)")] bexI 1);
  26.209 -by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 2);
  26.210 -by (simp_tac (!simpset addsimps [Filter_ex_def,ProjB_def,
  26.211 +by (asm_full_simp_tac (simpset() addsimps [compositionality_ex]) 2);
  26.212 +by (simp_tac (simpset() addsimps [Filter_ex_def,ProjB_def,
  26.213                                   lemma_2_1a,lemma_2_1b]) 1);
  26.214 -by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
  26.215 +by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
  26.216  by (pair_tac "ex" 1);
  26.217  by (etac conjE 1);
  26.218 -by (asm_full_simp_tac (!simpset addsimps [sch_actions_in_AorB]) 1);
  26.219 +by (asm_full_simp_tac (simpset() addsimps [sch_actions_in_AorB]) 1);
  26.220  
  26.221  (* <== *)
  26.222  
  26.223 @@ -485,16 +485,16 @@
  26.224  (* mkex actions are just the oracle *)
  26.225  by (pair_tac "exA" 1);
  26.226  by (pair_tac "exB" 1);
  26.227 -by (asm_full_simp_tac (!simpset addsimps [Mapfst_mkex_is_sch]) 1);
  26.228 +by (asm_full_simp_tac (simpset() addsimps [Mapfst_mkex_is_sch]) 1);
  26.229  
  26.230  (* mkex is an execution -- use compositionality on ex-level *)
  26.231 -by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 1);
  26.232 -by (asm_full_simp_tac (!simpset addsimps 
  26.233 +by (asm_full_simp_tac (simpset() addsimps [compositionality_ex]) 1);
  26.234 +by (asm_full_simp_tac (simpset() addsimps 
  26.235                   [stutter_mkex_on_A, stutter_mkex_on_B,
  26.236                    filter_mkex_is_exB,filter_mkex_is_exA]) 1);
  26.237  by (pair_tac "exA" 1);
  26.238  by (pair_tac "exB" 1);
  26.239 -by (asm_full_simp_tac (!simpset addsimps [mkex_actions_in_AorB]) 1);
  26.240 +by (asm_full_simp_tac (simpset() addsimps [mkex_actions_in_AorB]) 1);
  26.241  qed"compositionality_sch";
  26.242  
  26.243  
  26.244 @@ -507,9 +507,9 @@
  26.245  
  26.246  "Scheds (A||B) = par_scheds (Scheds A) (Scheds B)";
  26.247  
  26.248 -by (asm_full_simp_tac (!simpset addsimps [asig_of_par]) 1);
  26.249 +by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
  26.250  br set_ext 1;
  26.251 -by (asm_full_simp_tac (!simpset addsimps [compositionality_sch,actions_of_par]) 1);
  26.252 +by (asm_full_simp_tac (simpset() addsimps [compositionality_sch,actions_of_par]) 1);
  26.253  qed"compositionality_sch_modules";
  26.254  
  26.255  
    27.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Mon Nov 03 12:36:48 1997 +0100
    27.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Mon Nov 03 14:06:27 1997 +0100
    27.3 @@ -67,8 +67,8 @@
    27.4  \                             `schB))";
    27.5  by (rtac trans 1);
    27.6  by (stac mksch_unfold 1);
    27.7 -by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
    27.8 -by (simp_tac (!simpset addsimps [Cons_def]) 1);
    27.9 +by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
   27.10 +by (simp_tac (simpset() addsimps [Cons_def]) 1);
   27.11  qed"mksch_cons1";
   27.12  
   27.13  goal thy "!!x.[|x~:act A;x:act B|] \
   27.14 @@ -78,8 +78,8 @@
   27.15  \                            ))";
   27.16  by (rtac trans 1);
   27.17  by (stac mksch_unfold 1);
   27.18 -by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
   27.19 -by (simp_tac (!simpset addsimps [Cons_def]) 1);
   27.20 +by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
   27.21 +by (simp_tac (simpset() addsimps [Cons_def]) 1);
   27.22  qed"mksch_cons2";
   27.23  
   27.24  goal thy "!!x.[|x:act A;x:act B|] \
   27.25 @@ -91,8 +91,8 @@
   27.26  \             )";
   27.27  by (rtac trans 1);
   27.28  by (stac mksch_unfold 1);
   27.29 -by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
   27.30 -by (simp_tac (!simpset addsimps [Cons_def]) 1);
   27.31 +by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
   27.32 +by (simp_tac (simpset() addsimps [Cons_def]) 1);
   27.33  qed"mksch_cons3";
   27.34  
   27.35  val compotr_simps =[mksch_UU,mksch_nil, mksch_cons1,mksch_cons2,mksch_cons3];
   27.36 @@ -151,24 +151,24 @@
   27.37  \   --> Forall (%x. x:act (A||B)) (mksch A B`tr`schA`schB)";
   27.38  by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); 
   27.39  by (safe_tac set_cs);
   27.40 -by (asm_full_simp_tac (!simpset addsimps [actions_of_par]) 1);
   27.41 +by (asm_full_simp_tac (simpset() addsimps [actions_of_par]) 1);
   27.42  by (case_tac "a:act A" 1);
   27.43  by (case_tac "a:act B" 1);
   27.44  (* a:A, a:B *)
   27.45  by (Asm_full_simp_tac 1);
   27.46  by (rtac (Forall_Conc_impl RS mp) 1);
   27.47 -by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
   27.48 +by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
   27.49  by (rtac (Forall_Conc_impl RS mp) 1);
   27.50 -by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
   27.51 +by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
   27.52  (* a:A,a~:B *)
   27.53  by (Asm_full_simp_tac 1);
   27.54  by (rtac (Forall_Conc_impl RS mp) 1);
   27.55 -by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
   27.56 +by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
   27.57  by (case_tac "a:act B" 1);
   27.58  (* a~:A, a:B *)
   27.59  by (Asm_full_simp_tac 1);
   27.60  by (rtac (Forall_Conc_impl RS mp) 1);
   27.61 -by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
   27.62 +by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
   27.63  (* a~:A,a~:B *)
   27.64  by (Auto_tac());
   27.65  qed"ForallAorB_mksch1";
   27.66 @@ -182,7 +182,7 @@
   27.67  by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
   27.68  by (safe_tac set_cs);
   27.69  by (rtac (Forall_Conc_impl RS mp) 1);
   27.70 -by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,
   27.71 +by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,
   27.72                              intA_is_not_actB,int_is_act]) 1);
   27.73  qed"ForallBnA_mksch";
   27.74  
   27.75 @@ -197,7 +197,7 @@
   27.76  by (safe_tac set_cs);
   27.77  by (Asm_full_simp_tac 1);
   27.78  by (rtac (Forall_Conc_impl RS mp) 1);
   27.79 -by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,
   27.80 +by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,
   27.81                         intA_is_not_actB,int_is_act]) 1);
   27.82  qed"ForallAnB_mksch";
   27.83  
   27.84 @@ -217,7 +217,7 @@
   27.85  by (etac Seq_Finite_ind  1);
   27.86  by (Asm_full_simp_tac 1);
   27.87  (* main case *)
   27.88 -by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
   27.89 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
   27.90  by (safe_tac set_cs);
   27.91  
   27.92  (* a: act A; a: act B *)
   27.93 @@ -226,7 +226,7 @@
   27.94  back();
   27.95  by (REPEAT (etac conjE 1));
   27.96  (* Finite (tw iA x) and Finite (tw iB y) *)
   27.97 -by (asm_full_simp_tac (!simpset addsimps 
   27.98 +by (asm_full_simp_tac (simpset() addsimps 
   27.99            [not_ext_is_int_or_not_act,FiniteConc]) 1);
  27.100  (* now for conclusion IH applicable, but assumptions have to be transformed *)
  27.101  by (dres_inst_tac [("x","x"),
  27.102 @@ -236,7 +236,7 @@
  27.103                     ("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
  27.104  by (assume_tac 1);
  27.105  (* IH *)
  27.106 -by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
  27.107 +by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
  27.108                     FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
  27.109  
  27.110  (* a: act B; a~: act A *)
  27.111 @@ -244,14 +244,14 @@
  27.112  
  27.113  by (REPEAT (etac conjE 1));
  27.114  (* Finite (tw iB y) *)
  27.115 -by (asm_full_simp_tac (!simpset addsimps 
  27.116 +by (asm_full_simp_tac (simpset() addsimps 
  27.117            [not_ext_is_int_or_not_act,FiniteConc]) 1);
  27.118  (* now for conclusion IH applicable, but assumptions have to be transformed *)
  27.119  by (dres_inst_tac [("x","y"),
  27.120                     ("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
  27.121  by (assume_tac 1);
  27.122  (* IH *)
  27.123 -by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
  27.124 +by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
  27.125                     FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
  27.126  
  27.127  (* a~: act B; a: act A *)
  27.128 @@ -259,19 +259,19 @@
  27.129  
  27.130  by (REPEAT (etac conjE 1));
  27.131  (* Finite (tw iA x) *)
  27.132 -by (asm_full_simp_tac (!simpset addsimps 
  27.133 +by (asm_full_simp_tac (simpset() addsimps 
  27.134            [not_ext_is_int_or_not_act,FiniteConc]) 1);
  27.135  (* now for conclusion IH applicable, but assumptions have to be transformed *)
  27.136  by (dres_inst_tac [("x","x"),
  27.137                     ("g","Filter (%a. a:act A)`s")] subst_lemma2 1);
  27.138  by (assume_tac 1);
  27.139  (* IH *)
  27.140 -by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
  27.141 +by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
  27.142                     FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
  27.143  
  27.144  (* a~: act B; a~: act A *)
  27.145 -by (fast_tac (!claset addSIs [ext_is_act] 
  27.146 -                      addss (!simpset addsimps [externals_of_par]) ) 1);
  27.147 +by (fast_tac (claset() addSIs [ext_is_act] 
  27.148 +                      addss (simpset() addsimps [externals_of_par]) ) 1);
  27.149  qed"FiniteL_mksch";
  27.150  
  27.151  bind_thm("FiniteL_mksch1", FiniteL_mksch RS spec RS spec RS mp);
  27.152 @@ -310,10 +310,10 @@
  27.153                     ("g","Filter (%a. a:act B)`(s@@z)")] subst_lemma2 1);
  27.154  by (assume_tac 1);
  27.155  Addsimps [FilterConc]; 
  27.156 -by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
  27.157 +by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
  27.158  (* apply IH *)
  27.159  by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int B)`y)")] allE 1);
  27.160 -by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile])1);
  27.161 +by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile])1);
  27.162  by (REPEAT (etac exE 1));
  27.163  by (REPEAT (etac conjE 1));
  27.164  by (Asm_full_simp_tac 1); 
  27.165 @@ -324,9 +324,9 @@
  27.166  by (res_inst_tac [("x","Takewhile (%a. a:int B)`y @@ a>>y1")] exI 1);
  27.167  by (res_inst_tac [("x","y2")] exI 1);
  27.168  (* elminate all obligations up to two depending on Conc_assoc *)
  27.169 -by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, intA_is_not_actB,
  27.170 +by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, intA_is_not_actB,
  27.171               int_is_act,FilterPTakewhileQnil,int_is_not_ext]) 1); 
  27.172 -by (simp_tac (!simpset addsimps [Conc_assoc]) 1); 
  27.173 +by (simp_tac (simpset() addsimps [Conc_assoc]) 1); 
  27.174  qed"reduceA_mksch1";
  27.175  
  27.176  bind_thm("reduceA_mksch",conjI RSN (6,conjI RSN (5,reduceA_mksch1 RS spec RS mp)));
  27.177 @@ -365,10 +365,10 @@
  27.178                     ("g","Filter (%a. a:act A)`(s@@z)")] subst_lemma2 1);
  27.179  by (assume_tac 1);
  27.180  Addsimps [FilterConc]; 
  27.181 -by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
  27.182 +by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
  27.183  (* apply IH *)
  27.184  by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int A)`x)")] allE 1);
  27.185 -by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile])1);
  27.186 +by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile])1);
  27.187  by (REPEAT (etac exE 1));
  27.188  by (REPEAT (etac conjE 1));
  27.189  by (Asm_full_simp_tac 1); 
  27.190 @@ -379,9 +379,9 @@
  27.191  by (res_inst_tac [("x","Takewhile (%a. a:int A)`x @@ a>>x1")] exI 1);
  27.192  by (res_inst_tac [("x","x2")] exI 1);
  27.193  (* elminate all obligations up to two depending on Conc_assoc *)
  27.194 -by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, intA_is_not_actB,
  27.195 +by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, intA_is_not_actB,
  27.196               int_is_act,FilterPTakewhileQnil,int_is_not_ext]) 1); 
  27.197 -by (simp_tac (!simpset addsimps [Conc_assoc]) 1); 
  27.198 +by (simp_tac (simpset() addsimps [Conc_assoc]) 1); 
  27.199  qed"reduceB_mksch1";
  27.200  
  27.201  bind_thm("reduceB_mksch",conjI RSN (6,conjI RSN (5,reduceB_mksch1 RS spec RS mp)));
  27.202 @@ -398,7 +398,7 @@
  27.203  by (Auto_tac());
  27.204  by (Seq_case_simp_tac "tr" 1);
  27.205  (* tr = UU *)
  27.206 -by (asm_full_simp_tac (!simpset addsimps [nil_is_Conc]) 1);
  27.207 +by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc]) 1);
  27.208  (* tr = nil *)
  27.209  by (Auto_tac());
  27.210  (* tr = Conc *)
  27.211 @@ -408,17 +408,17 @@
  27.212  by (case_tac "s:act B" 1);
  27.213  by (rotate_tac ~2 1);
  27.214  by (rotate_tac ~2 2);
  27.215 -by (asm_full_simp_tac (!simpset addsimps [nil_is_Conc,nil_is_Conc2]) 1);
  27.216 -by (asm_full_simp_tac (!simpset addsimps [nil_is_Conc,nil_is_Conc2]) 1);
  27.217 +by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc,nil_is_Conc2]) 1);
  27.218 +by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc,nil_is_Conc2]) 1);
  27.219  by (case_tac "s:act B" 1);
  27.220  by (rotate_tac ~2 1);
  27.221 -by (asm_full_simp_tac (!simpset addsimps [nil_is_Conc,nil_is_Conc2]) 1);
  27.222 -by (fast_tac (!claset addSIs [ext_is_act] 
  27.223 -                      addss (!simpset addsimps [externals_of_par]) ) 1);
  27.224 +by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc,nil_is_Conc2]) 1);
  27.225 +by (fast_tac (claset() addSIs [ext_is_act] 
  27.226 +                      addss (simpset() addsimps [externals_of_par]) ) 1);
  27.227  (* main case *)
  27.228  by (Seq_case_simp_tac "tr" 1);
  27.229  (* tr = UU *)
  27.230 -by (asm_full_simp_tac (!simpset addsimps [Conc_Conc_eq]) 1);
  27.231 +by (asm_full_simp_tac (simpset() addsimps [Conc_Conc_eq]) 1);
  27.232  by (Auto_tac());
  27.233  (* tr = nil ok *)
  27.234  (* tr = Conc *)
  27.235 @@ -436,7 +436,7 @@
  27.236  by (asm_full_simp_tac (HOL_basic_ss addsimps [mksch_cons3]) 2);
  27.237  by (eres_inst_tac [("x","sb@@Takewhile (%a. a: int A)`a @@ Takewhile (%a. a:int B)`b@@(aaa>>nil)")] allE 2);
  27.238  by (eres_inst_tac [("x","sa")] allE 2);
  27.239 -by (asm_full_simp_tac (!simpset addsimps [Conc_assoc])2);
  27.240 +by (asm_full_simp_tac (simpset() addsimps [Conc_assoc])2);
  27.241  
  27.242  
  27.243  
  27.244 @@ -446,7 +446,7 @@
  27.245  by (case_tac "aaa:act B" 1);
  27.246  by (rotate_tac ~2 1);
  27.247  by (rotate_tac ~2 2);
  27.248 -by (asm_full_simp_tac (!simpset addsimps [Conc_Conc_eq]) 1);
  27.249 +by (asm_full_simp_tac (simpset() addsimps [Conc_Conc_eq]) 1);
  27.250  
  27.251  
  27.252  
  27.253 @@ -491,7 +491,7 @@
  27.254  
  27.255  (* main case *) 
  27.256  (* splitting into 4 cases according to a:A, a:B *)
  27.257 -by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
  27.258 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
  27.259  by (safe_tac set_cs);
  27.260  
  27.261  (* Case a:A, a:B *)
  27.262 @@ -500,7 +500,7 @@
  27.263  back();
  27.264  by (REPEAT (etac conjE 1));
  27.265  (* filtering internals of A in schA and of B in schB is nil *)
  27.266 -by (asm_full_simp_tac (!simpset addsimps 
  27.267 +by (asm_full_simp_tac (simpset() addsimps 
  27.268            [FilterPTakewhileQnil,not_ext_is_int_or_not_act,
  27.269             externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
  27.270  (* conclusion of IH ok, but assumptions of IH have to be transformed *)
  27.271 @@ -509,37 +509,37 @@
  27.272  by (dres_inst_tac [("x","schB")] subst_lemma1 1);
  27.273  by (assume_tac 1);
  27.274  (* IH *)
  27.275 -by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
  27.276 +by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
  27.277                     FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
  27.278  (* Case a:B, a~:A *)
  27.279  
  27.280  by (forward_tac [divide_Seq] 1);
  27.281  by (REPEAT (etac conjE 1));
  27.282  (* filtering internals of A is nil *)
  27.283 -by (asm_full_simp_tac (!simpset addsimps 
  27.284 +by (asm_full_simp_tac (simpset() addsimps 
  27.285            [FilterPTakewhileQnil,not_ext_is_int_or_not_act,
  27.286             externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
  27.287  by (dres_inst_tac [("x","schB")] subst_lemma1 1);
  27.288  back();
  27.289  by (assume_tac 1);
  27.290 -by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
  27.291 +by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
  27.292                      FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
  27.293  (* Case a:A, a~:B *)
  27.294  
  27.295  by (forward_tac [divide_Seq] 1);
  27.296  by (REPEAT (etac conjE 1));
  27.297  (* filtering internals of A is nil *)
  27.298 -by (asm_full_simp_tac (!simpset addsimps 
  27.299 +by (asm_full_simp_tac (simpset() addsimps 
  27.300            [FilterPTakewhileQnil,not_ext_is_int_or_not_act,
  27.301             externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
  27.302  by (dres_inst_tac [("x","schA")] subst_lemma1 1);
  27.303  by (assume_tac 1);
  27.304 -by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
  27.305 +by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
  27.306                      FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
  27.307  (* Case a~:A, a~:B *)
  27.308  
  27.309 -by (fast_tac (!claset addSIs [ext_is_act] 
  27.310 -                      addss (!simpset addsimps [externals_of_par]) ) 1);
  27.311 +by (fast_tac (claset() addSIs [ext_is_act] 
  27.312 +                      addss (simpset() addsimps [externals_of_par]) ) 1);
  27.313  qed"FilterA_mksch_is_tr";
  27.314  
  27.315  
  27.316 @@ -573,13 +573,13 @@
  27.317  by (subgoal_tac "schA=nil" 1);
  27.318  by (Asm_simp_tac 1);
  27.319  (* first side: mksch = nil *)
  27.320 -by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPnil,ForallBnAmksch,FiniteL_mksch],
  27.321 -                           !simpset)) 1);
  27.322 +by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil,ForallBnAmksch,FiniteL_mksch],
  27.323 +                           simpset())) 1);
  27.324  (* second side: schA = nil *)
  27.325  by (eres_inst_tac [("A","A")] LastActExtimplnil 1);
  27.326  by (Asm_simp_tac 1);
  27.327 -by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPnil],
  27.328 -                           !simpset)) 1);
  27.329 +by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil],
  27.330 +                           simpset())) 1);
  27.331  
  27.332  (* case ~ Finite s *)
  27.333  
  27.334 @@ -587,15 +587,15 @@
  27.335  by (subgoal_tac "schA=UU" 1);
  27.336  by (Asm_simp_tac 1);
  27.337  (* first side: mksch = UU *)
  27.338 -by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPUU,
  27.339 +by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU,
  27.340                                             (finiteR_mksch RS mp COMP rev_contrapos),
  27.341                                              ForallBnAmksch],
  27.342 -                           !simpset)) 1);
  27.343 +                           simpset())) 1);
  27.344  (* schA = UU *)
  27.345  by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
  27.346  by (Asm_simp_tac 1);
  27.347 -by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPUU],
  27.348 -                           !simpset)) 1);
  27.349 +by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU],
  27.350 +                           simpset())) 1);
  27.351  
  27.352  (* case" ~ Forall (%x.x:act B & x~:act A) s" *)
  27.353  
  27.354 @@ -649,7 +649,7 @@
  27.355  by (rtac take_reduction 1);
  27.356  
  27.357  (* f A (tw iA) = tw ~eA *)
  27.358 -by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
  27.359 +by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
  27.360                                not_ext_is_int_or_not_act]) 1);
  27.361  by (rtac refl 1);
  27.362  
  27.363 @@ -661,12 +661,12 @@
  27.364  
  27.365  *)
  27.366  (* assumption schB *)
  27.367 -by (asm_full_simp_tac (!simpset addsimps [ext_and_act]) 1);
  27.368 +by (asm_full_simp_tac (simpset() addsimps [ext_and_act]) 1);
  27.369  (* assumption schA *)
  27.370  by (dres_inst_tac [("x","schA"),
  27.371                     ("g","Filter (%a. a:act A)`s2")] subst_lemma2 1);
  27.372  by (assume_tac 1);
  27.373 -by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil]) 1);
  27.374 +by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil]) 1);
  27.375  (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
  27.376  by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
  27.377  by (dres_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
  27.378 @@ -725,8 +725,8 @@
  27.379  by (subgoal_tac "schA=nil" 1);
  27.380  by (Asm_simp_tac 1);
  27.381  (* first side: mksch = nil *)
  27.382 -by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPnil,ForallBnAmksch,FiniteL_mksch1],
  27.383 -                           !simpset)) 1);
  27.384 +by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil,ForallBnAmksch,FiniteL_mksch1],
  27.385 +                           simpset())) 1);
  27.386  (* second side: schA = nil *)
  27.387  by (eres_inst_tac [("A","A")] LastActExtimplnil 1);
  27.388  by (Asm_simp_tac 1);
  27.389 @@ -740,10 +740,10 @@
  27.390  by (subgoal_tac "schA=UU" 1);
  27.391  by (Asm_simp_tac 1);
  27.392  (* first side: mksch = UU *)
  27.393 -by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPUU,
  27.394 +by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU,
  27.395                                             (finiteR_mksch RS mp COMP rev_contrapos),
  27.396                                              ForallBnAmksch],
  27.397 -                           !simpset)) 1);
  27.398 +                           simpset())) 1);
  27.399  (* schA = UU *)
  27.400  by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
  27.401  by (Asm_simp_tac 1);
  27.402 @@ -807,25 +807,25 @@
  27.403  by (rtac take_reduction 1);
  27.404  
  27.405  (* f A (tw iA) = tw ~eA *)
  27.406 -by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
  27.407 +by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
  27.408                                not_ext_is_int_or_not_act]) 1);
  27.409  by (rtac refl 1);
  27.410 -by (asm_full_simp_tac (!simpset addsimps [int_is_act,
  27.411 +by (asm_full_simp_tac (simpset() addsimps [int_is_act,
  27.412                                not_ext_is_int_or_not_act]) 1);
  27.413  by (rotate_tac ~11 1);
  27.414  
  27.415  (* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
  27.416  
  27.417  (* assumption Forall tr *)
  27.418 -by (asm_full_simp_tac (!simpset addsimps [Forall_Conc]) 1);
  27.419 +by (asm_full_simp_tac (simpset() addsimps [Forall_Conc]) 1);
  27.420  (* assumption schB *)
  27.421 -by (asm_full_simp_tac (!simpset addsimps [Forall_Conc,ext_and_act]) 1);
  27.422 +by (asm_full_simp_tac (simpset() addsimps [Forall_Conc,ext_and_act]) 1);
  27.423  by (REPEAT (etac conjE 1));
  27.424  (* assumption schA *)
  27.425  by (dres_inst_tac [("x","schA"),
  27.426                     ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
  27.427  by (assume_tac 1);
  27.428 -by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
  27.429 +by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
  27.430  (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
  27.431  by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
  27.432  by (forw_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
  27.433 @@ -835,7 +835,7 @@
  27.434  by (dres_inst_tac [("s","schA"),
  27.435                     ("P","Forall (%x. x:act A)")] subst 1);
  27.436  by (assume_tac 1);
  27.437 -by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
  27.438 +by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, int_is_act]) 1);
  27.439  
  27.440  (* case x:actions(asig_of A) & x: actions(asig_of B) *)
  27.441  
  27.442 @@ -863,12 +863,12 @@
  27.443  by (assume_tac 1);
  27.444  
  27.445  (* f A (tw iA) = tw ~eA *)
  27.446 -by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
  27.447 +by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
  27.448                                not_ext_is_int_or_not_act]) 1);
  27.449  
  27.450  (* rewrite assumption forall and schB *)
  27.451  by (rotate_tac 13 1);
  27.452 -by (asm_full_simp_tac (!simpset addsimps [ext_and_act]) 1);
  27.453 +by (asm_full_simp_tac (simpset() addsimps [ext_and_act]) 1);
  27.454  
  27.455  (* divide_Seq for schB2 *)
  27.456  by (forw_inst_tac [("y","y2")] (sym RS antisym_less_inverse RS conjunct1 RS divide_Seq) 1);
  27.457 @@ -877,10 +877,10 @@
  27.458  by (dres_inst_tac [("x","schA"),
  27.459                     ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
  27.460  by (assume_tac 1);
  27.461 -by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
  27.462 +by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
  27.463  
  27.464  (* f A (tw iB schB2) = nil *) 
  27.465 -by (asm_full_simp_tac (!simpset addsimps [int_is_not_ext,not_ext_is_int_or_not_act,
  27.466 +by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext,not_ext_is_int_or_not_act,
  27.467               FilterPTakewhileQnil,intA_is_not_actB]) 1);
  27.468  
  27.469  
  27.470 @@ -895,7 +895,7 @@
  27.471  by (dres_inst_tac [("x","y2"),
  27.472                     ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
  27.473  by (assume_tac 1);
  27.474 -by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
  27.475 +by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
  27.476  
  27.477  (* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
  27.478  by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
  27.479 @@ -904,7 +904,7 @@
  27.480  by (dres_inst_tac [("sch","y2"),("P","%a. a:int B")] LastActExtsmall1 1);
  27.481  
  27.482  (* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
  27.483 -by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile]) 1);
  27.484 +by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile]) 1);
  27.485  
  27.486  (* case x~:A & x:B  *)
  27.487  (* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
  27.488 @@ -915,9 +915,9 @@
  27.489  (* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
  27.490  by (rotate_tac ~9 1);
  27.491  (* reduce forall assumption from tr to (x>>rs) *)
  27.492 -by (asm_full_simp_tac (!simpset addsimps [externals_of_par]) 1);
  27.493 +by (asm_full_simp_tac (simpset() addsimps [externals_of_par]) 1);
  27.494  by (REPEAT (etac conjE 1));
  27.495 -by (fast_tac (!claset addSIs [ext_is_act]) 1);
  27.496 +by (fast_tac (claset() addSIs [ext_is_act]) 1);
  27.497  
  27.498  qed"FilterAmksch_is_schA";
  27.499  
  27.500 @@ -967,8 +967,8 @@
  27.501  by (subgoal_tac "schB=nil" 1);
  27.502  by (Asm_simp_tac 1);
  27.503  (* first side: mksch = nil *)
  27.504 -by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPnil,ForallAnBmksch,FiniteL_mksch1],
  27.505 -                           !simpset)) 1);
  27.506 +by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil,ForallAnBmksch,FiniteL_mksch1],
  27.507 +                           simpset())) 1);
  27.508  (* second side: schA = nil *)
  27.509  by (eres_inst_tac [("A","B")] LastActExtimplnil 1);
  27.510  by (Asm_simp_tac 1);
  27.511 @@ -982,10 +982,10 @@
  27.512  by (subgoal_tac "schB=UU" 1);
  27.513  by (Asm_simp_tac 1);
  27.514  (* first side: mksch = UU *)
  27.515 -by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPUU,
  27.516 +by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU,
  27.517                                             (finiteR_mksch RS mp COMP rev_contrapos),
  27.518                                              ForallAnBmksch],
  27.519 -                           !simpset)) 1);
  27.520 +                           simpset())) 1);
  27.521  (* schA = UU *)
  27.522  by (eres_inst_tac [("A","B")] LastActExtimplUU 1);
  27.523  by (Asm_simp_tac 1);
  27.524 @@ -1049,25 +1049,25 @@
  27.525  by (rtac take_reduction 1);
  27.526  
  27.527  (* f B (tw iB) = tw ~eB *)
  27.528 -by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
  27.529 +by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
  27.530                                not_ext_is_int_or_not_act]) 1);
  27.531  by (rtac refl 1);
  27.532 -by (asm_full_simp_tac (!simpset addsimps [int_is_act,
  27.533 +by (asm_full_simp_tac (simpset() addsimps [int_is_act,
  27.534                                not_ext_is_int_or_not_act]) 1);
  27.535  by (rotate_tac ~11 1);
  27.536  
  27.537  (* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
  27.538  
  27.539  (* assumption Forall tr *)
  27.540 -by (asm_full_simp_tac (!simpset addsimps [Forall_Conc]) 1);
  27.541 +by (asm_full_simp_tac (simpset() addsimps [Forall_Conc]) 1);
  27.542  (* assumption schA *)
  27.543 -by (asm_full_simp_tac (!simpset addsimps [Forall_Conc,ext_and_act]) 1);
  27.544 +by (asm_full_simp_tac (simpset() addsimps [Forall_Conc,ext_and_act]) 1);
  27.545  by (REPEAT (etac conjE 1));
  27.546  (* assumption schB *)
  27.547  by (dres_inst_tac [("x","schB"),
  27.548                     ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
  27.549  by (assume_tac 1);
  27.550 -by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
  27.551 +by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
  27.552  (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
  27.553  by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1);
  27.554  by (forw_inst_tac [("sch1.0","x1")]  LastActExtsmall2 1);
  27.555 @@ -1077,7 +1077,7 @@
  27.556  by (dres_inst_tac [("s","schB"),
  27.557                     ("P","Forall (%x. x:act B)")] subst 1);
  27.558  by (assume_tac 1);
  27.559 -by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
  27.560 +by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, int_is_act]) 1);
  27.561  
  27.562  (* case x:actions(asig_of A) & x: actions(asig_of B) *)
  27.563  
  27.564 @@ -1105,12 +1105,12 @@
  27.565  by (assume_tac 1);
  27.566  
  27.567  (* f B (tw iB) = tw ~eB *)
  27.568 -by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
  27.569 +by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
  27.570                                not_ext_is_int_or_not_act]) 1);
  27.571  
  27.572  (* rewrite assumption forall and schB *)
  27.573  by (rotate_tac 13 1);
  27.574 -by (asm_full_simp_tac (!simpset addsimps [ext_and_act]) 1);
  27.575 +by (asm_full_simp_tac (simpset() addsimps [ext_and_act]) 1);
  27.576  
  27.577  (* divide_Seq for schB2 *)
  27.578  by (forw_inst_tac [("y","x2")] (sym RS antisym_less_inverse RS conjunct1 RS divide_Seq) 1);
  27.579 @@ -1119,10 +1119,10 @@
  27.580  by (dres_inst_tac [("x","schB"),
  27.581                     ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
  27.582  by (assume_tac 1);
  27.583 -by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
  27.584 +by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
  27.585  
  27.586  (* f B (tw iA schA2) = nil *) 
  27.587 -by (asm_full_simp_tac (!simpset addsimps [int_is_not_ext,not_ext_is_int_or_not_act,
  27.588 +by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext,not_ext_is_int_or_not_act,
  27.589               FilterPTakewhileQnil,intA_is_not_actB]) 1);
  27.590  
  27.591  
  27.592 @@ -1137,7 +1137,7 @@
  27.593  by (dres_inst_tac [("x","x2"),
  27.594                     ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
  27.595  by (assume_tac 1);
  27.596 -by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
  27.597 +by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
  27.598  
  27.599  (* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
  27.600  by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1);
  27.601 @@ -1146,7 +1146,7 @@
  27.602  by (dres_inst_tac [("sch","x2"),("P","%a. a:int A")] LastActExtsmall1 1);
  27.603  
  27.604  (* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
  27.605 -by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile]) 1);
  27.606 +by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile]) 1);
  27.607  
  27.608  (* case x~:B & x:A  *)
  27.609  (* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
  27.610 @@ -1157,9 +1157,9 @@
  27.611  (* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
  27.612  by (rotate_tac ~9 1);
  27.613  (* reduce forall assumption from tr to (x>>rs) *)
  27.614 -by (asm_full_simp_tac (!simpset addsimps [externals_of_par]) 1);
  27.615 +by (asm_full_simp_tac (simpset() addsimps [externals_of_par]) 1);
  27.616  by (REPEAT (etac conjE 1));
  27.617 -by (fast_tac (!claset addSIs [ext_is_act]) 1);
  27.618 +by (fast_tac (claset() addSIs [ext_is_act]) 1);
  27.619  
  27.620  qed"FilterBmksch_is_schB";
  27.621  
  27.622 @@ -1177,19 +1177,19 @@
  27.623  \             Filter (%a. a:act B)`tr : traces B &\
  27.624  \             Forall (%x. x:ext(A||B)) tr)";
  27.625  
  27.626 -by (simp_tac (!simpset addsimps [traces_def,has_trace_def]) 1);
  27.627 +by (simp_tac (simpset() addsimps [traces_def,has_trace_def]) 1);
  27.628  by (safe_tac set_cs);
  27.629   
  27.630  (* ==> *) 
  27.631  (* There is a schedule of A *)
  27.632  by (res_inst_tac [("x","Filter (%a. a:act A)`sch")] bexI 1);
  27.633 -by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 2);
  27.634 -by (asm_full_simp_tac (!simpset addsimps [compatibility_consequence1,
  27.635 +by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 2);
  27.636 +by (asm_full_simp_tac (simpset() addsimps [compatibility_consequence1,
  27.637                    externals_of_par,ext1_ext2_is_not_act1]) 1);
  27.638  (* There is a schedule of B *)
  27.639  by (res_inst_tac [("x","Filter (%a. a:act B)`sch")] bexI 1);
  27.640 -by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 2);
  27.641 -by (asm_full_simp_tac (!simpset addsimps [compatibility_consequence2,
  27.642 +by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 2);
  27.643 +by (asm_full_simp_tac (simpset() addsimps [compatibility_consequence2,
  27.644                    externals_of_par,ext1_ext2_is_not_act2]) 1);
  27.645  (* Traces of A||B have only external actions from A or B *)  
  27.646  by (rtac ForallPFilterP 1);
  27.647 @@ -1215,11 +1215,11 @@
  27.648  by (res_inst_tac [("x","mksch A B`tr`schA`schB")] bexI 1);
  27.649  
  27.650  (* External actions of mksch are just the oracle *)
  27.651 -by (asm_full_simp_tac (!simpset addsimps [FilterA_mksch_is_tr RS spec RS spec RS mp]) 1);
  27.652 +by (asm_full_simp_tac (simpset() addsimps [FilterA_mksch_is_tr RS spec RS spec RS mp]) 1);
  27.653  
  27.654  (* mksch is a schedule -- use compositionality on sch-level *)
  27.655 -by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 1);
  27.656 -by (asm_full_simp_tac (!simpset addsimps [FilterAmksch_is_schA,FilterBmksch_is_schB]) 1);
  27.657 +by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 1);
  27.658 +by (asm_full_simp_tac (simpset() addsimps [FilterAmksch_is_schA,FilterBmksch_is_schB]) 1);
  27.659  by (etac ForallAorB_mksch 1);
  27.660  by (etac ForallPForallQ 1);
  27.661  by (etac ext_is_act 1);
  27.662 @@ -1238,9 +1238,9 @@
  27.663  \           is_asig(asig_of A); is_asig(asig_of B)|] \
  27.664  \==> Traces (A||B) = par_traces (Traces A) (Traces B)";
  27.665  
  27.666 -by (asm_full_simp_tac (!simpset addsimps [asig_of_par]) 1);
  27.667 +by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
  27.668  br set_ext 1;
  27.669 -by (asm_full_simp_tac (!simpset addsimps [compositionality_tr,externals_of_par]) 1);
  27.670 +by (asm_full_simp_tac (simpset() addsimps [compositionality_tr,externals_of_par]) 1);
  27.671  qed"compositionality_tr_modules";
  27.672  
  27.673  
    28.1 --- a/src/HOLCF/IOA/meta_theory/Compositionality.ML	Mon Nov 03 12:36:48 1997 +0100
    28.2 +++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML	Mon Nov 03 14:06:27 1997 +0100
    28.3 @@ -20,7 +20,7 @@
    28.4  (* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q`tr = Filter R`tr *)
    28.5  by (assume_tac 2);
    28.6  by (rtac compatibility_consequence3 1);
    28.7 -by (REPEAT (asm_full_simp_tac (!simpset 
    28.8 +by (REPEAT (asm_full_simp_tac (simpset() 
    28.9                    addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1));
   28.10  qed"Filter_actAisFilter_extA";
   28.11  
   28.12 @@ -38,7 +38,7 @@
   28.13  by (rtac ForallPFilterQR 1);
   28.14  by (assume_tac 2);
   28.15  by (rtac compatibility_consequence4 1);
   28.16 -by (REPEAT (asm_full_simp_tac (!simpset 
   28.17 +by (REPEAT (asm_full_simp_tac (simpset() 
   28.18                    addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1));
   28.19  qed"Filter_actAisFilter_extA2";
   28.20  
   28.21 @@ -58,29 +58,29 @@
   28.22  \            B1 =<| B2 |] \
   28.23  \        ==> (A1 || B1) =<| (A2 || B2)";
   28.24  
   28.25 -by (asm_full_simp_tac (!simpset addsimps [is_asig_of_def]) 1);
   28.26 +by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def]) 1);
   28.27  by (forw_inst_tac [("A2","A1")] (compat_commute RS iffD1) 1);
   28.28  by (forw_inst_tac [("A2","A2")] (compat_commute RS iffD1) 1);
   28.29 -by (asm_full_simp_tac (!simpset addsimps [ioa_implements_def,
   28.30 +by (asm_full_simp_tac (simpset() addsimps [ioa_implements_def,
   28.31            inputs_of_par,outputs_of_par,externals_of_par]) 1);
   28.32  by (safe_tac set_cs);
   28.33 -by (asm_full_simp_tac (!simpset addsimps [compositionality_tr]) 1);
   28.34 +by (asm_full_simp_tac (simpset() addsimps [compositionality_tr]) 1);
   28.35  by (subgoal_tac "ext A1 = ext A2 & ext B1 = ext B2" 1);
   28.36 -by (asm_full_simp_tac (!simpset addsimps [externals_def]) 2);
   28.37 +by (asm_full_simp_tac (simpset() addsimps [externals_def]) 2);
   28.38  by (REPEAT (etac conjE 1));
   28.39  (* rewrite with proven subgoal *)
   28.40 -by (asm_full_simp_tac (!simpset addsimps [externals_of_par]) 1);
   28.41 +by (asm_full_simp_tac (simpset() addsimps [externals_of_par]) 1);
   28.42  by (safe_tac set_cs);
   28.43  
   28.44  (* 2 goals, the 3rd has been solved automatically *)
   28.45  (* 1: Filter A2 x : traces A2 *)
   28.46  by (dres_inst_tac [("A","traces A1")] subsetD 1);
   28.47  by (assume_tac 1);
   28.48 -by (asm_full_simp_tac (!simpset addsimps [Filter_actAisFilter_extA]) 1);
   28.49 +by (asm_full_simp_tac (simpset() addsimps [Filter_actAisFilter_extA]) 1);
   28.50  (* 2: Filter B2 x : traces B2 *)
   28.51  by (dres_inst_tac [("A","traces B1")] subsetD 1);
   28.52  by (assume_tac 1);
   28.53 -by (asm_full_simp_tac (!simpset addsimps [Filter_actAisFilter_extA2]) 1);
   28.54 +by (asm_full_simp_tac (simpset() addsimps [Filter_actAisFilter_extA2]) 1);
   28.55  qed"compositionality";
   28.56  
   28.57  
    29.1 --- a/src/HOLCF/IOA/meta_theory/Deadlock.ML	Mon Nov 03 12:36:48 1997 +0100
    29.2 +++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML	Mon Nov 03 14:06:27 1997 +0100
    29.3 @@ -12,14 +12,14 @@
    29.4  
    29.5  goal thy "!! sch. [| Filter (%x. x:act A)`sch : schedules A; a:inp A; input_enabled A; Finite sch|] \
    29.6  \         ==> Filter (%x. x:act A)`sch @@ a>>nil : schedules A";
    29.7 -by (asm_full_simp_tac (!simpset addsimps [schedules_def,has_schedule_def]) 1);
    29.8 +by (asm_full_simp_tac (simpset() addsimps [schedules_def,has_schedule_def]) 1);
    29.9  by (safe_tac set_cs);
   29.10  by (forward_tac  [inp_is_act] 1);
   29.11 -by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
   29.12 +by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
   29.13  by (pair_tac "ex" 1);
   29.14  ren "sch s ex" 1;
   29.15  by (subgoal_tac "Finite ex" 1);
   29.16 -by (asm_full_simp_tac (!simpset addsimps [filter_act_def]) 2);
   29.17 +by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 2);
   29.18  by (rtac (Map2Finite RS iffD1) 2);
   29.19  by (res_inst_tac [("t","Map fst`ex")] subst 2);
   29.20  by (assume_tac 2);
   29.21 @@ -29,7 +29,7 @@
   29.22  by (etac allE 1);
   29.23  by (etac exE 1);
   29.24  (* using input-enabledness *)
   29.25 -by (asm_full_simp_tac (!simpset addsimps [input_enabled_def]) 1);
   29.26 +by (asm_full_simp_tac (simpset() addsimps [input_enabled_def]) 1);
   29.27  by (REPEAT (etac conjE 1));
   29.28  by (eres_inst_tac [("x","a")] allE 1);
   29.29  by (Asm_full_simp_tac 1);
   29.30 @@ -37,7 +37,7 @@
   29.31  by (etac exE 1);
   29.32  (* instantiate execution *)
   29.33  by (res_inst_tac [("x","(s,ex @@ (a,s2)>>nil)")] exI 1);
   29.34 -by (asm_full_simp_tac (!simpset addsimps [filter_act_def,MapConc]) 1);
   29.35 +by (asm_full_simp_tac (simpset() addsimps [filter_act_def,MapConc]) 1);
   29.36  by (eres_inst_tac [("t","u")] lemma_2_1 1);
   29.37  by (Asm_full_simp_tac 1);
   29.38  by (rtac sym 1);
   29.39 @@ -55,10 +55,10 @@
   29.40  \            Filter (%x. x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
   29.41  \          ==> (sch @@ a>>nil) : schedules (A||B)";
   29.42  
   29.43 -by (asm_full_simp_tac (!simpset addsimps [compositionality_sch,locals_def]) 1);
   29.44 +by (asm_full_simp_tac (simpset() addsimps [compositionality_sch,locals_def]) 1);
   29.45  by (rtac conjI 1);
   29.46  (* a : act (A||B) *)
   29.47 -by (asm_full_simp_tac (!simpset addsimps [actions_of_par]) 2);
   29.48 +by (asm_full_simp_tac (simpset() addsimps [actions_of_par]) 2);
   29.49  by (rtac disjI1 2);
   29.50  by (etac disjE 2);
   29.51  by (etac int_is_act 2);
    30.1 --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Mon Nov 03 12:36:48 1997 +0100
    30.2 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Mon Nov 03 14:06:27 1997 +0100
    30.3 @@ -27,7 +27,7 @@
    30.4  by (rtac fix_eq2 1);
    30.5  by (rtac corresp_exC_def 1);
    30.6  by (rtac beta_cfun 1);
    30.7 -by (simp_tac (!simpset addsimps [flift1_def]) 1);
    30.8 +by (simp_tac (simpset() addsimps [flift1_def]) 1);
    30.9  qed"corresp_exC_unfold";
   30.10  
   30.11  goal thy "(corresp_exC A f`UU) s=UU";
   30.12 @@ -45,7 +45,7 @@
   30.13  \          @@ ((corresp_exC A f`xs) (snd at))";
   30.14  by (rtac trans 1);
   30.15  by (stac corresp_exC_unfold 1);
   30.16 -by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1);
   30.17 +by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
   30.18  by (Simp_tac 1);
   30.19  qed"corresp_exC_cons";
   30.20  
   30.21 @@ -77,7 +77,7 @@
   30.22  \    is_exec_frag A (f s,@x. move A x (f s) a (f t))";
   30.23  by (cut_inst_tac [] move_is_move 1);
   30.24  by (REPEAT (assume_tac 1));
   30.25 -by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
   30.26 +by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
   30.27  qed"move_subprop1";
   30.28  
   30.29  goal thy
   30.30 @@ -85,7 +85,7 @@
   30.31  \    Finite ((@x. move A x (f s) a (f t)))";
   30.32  by (cut_inst_tac [] move_is_move 1);
   30.33  by (REPEAT (assume_tac 1));
   30.34 -by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
   30.35 +by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
   30.36  qed"move_subprop2";
   30.37  
   30.38  goal thy
   30.39 @@ -93,7 +93,7 @@
   30.40  \    laststate (f s,@x. move A x (f s) a (f t)) = (f t)";
   30.41  by (cut_inst_tac [] move_is_move 1);
   30.42  by (REPEAT (assume_tac 1));
   30.43 -by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
   30.44 +by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
   30.45  qed"move_subprop3";
   30.46  
   30.47  goal thy
   30.48 @@ -103,7 +103,7 @@
   30.49  
   30.50  by (cut_inst_tac [] move_is_move 1);
   30.51  by (REPEAT (assume_tac 1));
   30.52 -by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
   30.53 +by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
   30.54  qed"move_subprop4";
   30.55  
   30.56  
   30.57 @@ -120,7 +120,7 @@
   30.58  
   30.59  
   30.60  goal thy "mk_trace C`(ex1 @@ ex2)= (mk_trace C`ex1) @@ (mk_trace C`ex2)";
   30.61 -by (simp_tac (!simpset addsimps [mk_trace_def,filter_act_def,
   30.62 +by (simp_tac (simpset() addsimps [mk_trace_def,filter_act_def,
   30.63                                   FilterConc,MapConc]) 1);
   30.64  qed"mk_traceConc";
   30.65  
   30.66 @@ -138,12 +138,12 @@
   30.67  by (pair_induct_tac "xs" [is_exec_frag_def] 1);
   30.68  (* cons case *) 
   30.69  by (safe_tac set_cs);
   30.70 -by (asm_full_simp_tac (!simpset addsimps [mk_traceConc]) 1);
   30.71 +by (asm_full_simp_tac (simpset() addsimps [mk_traceConc]) 1);
   30.72  by (forward_tac [reachable.reachable_n] 1);
   30.73  by (assume_tac 1);
   30.74  by (eres_inst_tac [("x","y")] allE 1);
   30.75  by (Asm_full_simp_tac 1);
   30.76 -by (asm_full_simp_tac (!simpset addsimps [move_subprop4] 
   30.77 +by (asm_full_simp_tac (simpset() addsimps [move_subprop4] 
   30.78                            setloop split_tac [expand_if] ) 1);
   30.79  qed"lemma_1";
   30.80  
   30.81 @@ -224,7 +224,7 @@
   30.82    "!!f. [| ext C = ext A; is_ref_map f C A |] \
   30.83  \          ==> traces C <= traces A"; 
   30.84  
   30.85 -  by (simp_tac(!simpset addsimps [has_trace_def2])1);
   30.86 +  by (simp_tac(simpset() addsimps [has_trace_def2])1);
   30.87    by (safe_tac set_cs);
   30.88  
   30.89    (* give execution of abstract automata *)
   30.90 @@ -234,17 +234,17 @@
   30.91    by (pair_tac "ex" 1);
   30.92    by (etac (lemma_1 RS spec RS mp) 1);
   30.93    by (REPEAT (atac 1));
   30.94 -  by (asm_full_simp_tac (!simpset addsimps [executions_def,reachable.reachable_0]) 1);
   30.95 +  by (asm_full_simp_tac (simpset() addsimps [executions_def,reachable.reachable_0]) 1);
   30.96   
   30.97    (* corresp_ex is execution, Lemma 2 *)
   30.98    by (pair_tac "ex" 1);
   30.99 -  by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
  30.100 +  by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
  30.101    (* start state *) 
  30.102    by (rtac conjI 1);
  30.103 -  by (asm_full_simp_tac (!simpset addsimps [is_ref_map_def,corresp_ex_def]) 1);
  30.104 +  by (asm_full_simp_tac (simpset() addsimps [is_ref_map_def,corresp_ex_def]) 1);
  30.105    (* is-execution-fragment *)
  30.106    by (etac (lemma_2 RS spec RS mp) 1);
  30.107 -  by (asm_full_simp_tac (!simpset addsimps [reachable.reachable_0]) 1);
  30.108 +  by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
  30.109  qed"trace_inclusion"; 
  30.110  
  30.111  
    31.1 --- a/src/HOLCF/IOA/meta_theory/RefMappings.ML	Mon Nov 03 12:36:48 1997 +0100
    31.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Mon Nov 03 14:06:27 1997 +0100
    31.3 @@ -13,15 +13,15 @@
    31.4  (* ---------------------------------------------------------------------------- *)
    31.5  
    31.6  goal thy "laststate (s,UU) = s";
    31.7 -by (simp_tac (!simpset addsimps [laststate_def]) 1); 
    31.8 +by (simp_tac (simpset() addsimps [laststate_def]) 1); 
    31.9  qed"laststate_UU";
   31.10  
   31.11  goal thy "laststate (s,nil) = s";
   31.12 -by (simp_tac (!simpset addsimps [laststate_def]) 1);
   31.13 +by (simp_tac (simpset() addsimps [laststate_def]) 1);
   31.14  qed"laststate_nil";
   31.15  
   31.16  goal thy "!! ex. Finite ex ==> laststate (s,at>>ex) = laststate (snd at,ex)";
   31.17 -by (simp_tac (!simpset addsimps [laststate_def]) 1);
   31.18 +by (simp_tac (simpset() addsimps [laststate_def]) 1);
   31.19  by (case_tac "ex=nil" 1);
   31.20  by (Asm_simp_tac 1);
   31.21  by (Asm_simp_tac 1);
   31.22 @@ -45,14 +45,14 @@
   31.23  goal thy"!!f. s -a--A-> t ==> ? ex. move A ex s a t";
   31.24  
   31.25  by (res_inst_tac [("x","(a,t)>>nil")] exI 1);
   31.26 -by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
   31.27 +by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
   31.28  qed"transition_is_ex";
   31.29   
   31.30  
   31.31  goal thy"!!f. (~a:ext A) & s=t ==> ? ex. move A ex s a t";
   31.32  
   31.33  by (res_inst_tac [("x","nil")] exI 1);
   31.34 -by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
   31.35 +by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
   31.36  qed"nothing_is_ex";
   31.37  
   31.38  
   31.39 @@ -60,7 +60,7 @@
   31.40  \        ==> ? ex. move A ex s a s''";
   31.41  
   31.42  by (res_inst_tac [("x","(a,s')>>(a',s'')>>nil")] exI 1);
   31.43 -by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
   31.44 +by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
   31.45  qed"ei_transitions_are_ex";
   31.46  
   31.47  
   31.48 @@ -70,7 +70,7 @@
   31.49  \     ? ex. move A ex s1 a1 s4";
   31.50    
   31.51  by (res_inst_tac [("x","(a1,s2)>>(a2,s3)>>(a3,s4)>>nil")] exI 1);
   31.52 -by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
   31.53 +by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
   31.54  qed"eii_transitions_are_ex";
   31.55  
   31.56  
   31.57 @@ -92,23 +92,23 @@
   31.58  
   31.59  
   31.60  val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
   31.61 -  by(fast_tac (!claset addDs prems) 1);
   31.62 +  by(fast_tac (claset() addDs prems) 1);
   31.63  val lemma = result();
   31.64  
   31.65  
   31.66  goal thy "!!f.[| is_weak_ref_map f C A |]\
   31.67  \                      ==> (is_weak_ref_map f (rename C g) (rename A g))";
   31.68 -by (asm_full_simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
   31.69 +by (asm_full_simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
   31.70  by (rtac conjI 1);
   31.71  (* 1: start states *)
   31.72 -by (asm_full_simp_tac (!simpset addsimps [rename_def,rename_set_def,starts_of_def]) 1);
   31.73 +by (asm_full_simp_tac (simpset() addsimps [rename_def,rename_set_def,starts_of_def]) 1);
   31.74  (* 2: reachable transitions *)
   31.75  by (REPEAT (rtac allI 1));
   31.76  by (rtac lemma 1);
   31.77 -by (simp_tac (!simpset addsimps [rename_def,rename_set_def]) 1);
   31.78 -by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_inputs_def,
   31.79 +by (simp_tac (simpset() addsimps [rename_def,rename_set_def]) 1);
   31.80 +by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,
   31.81  asig_outputs_def,asig_of_def,trans_of_def]) 1);
   31.82 -by (safe_tac (!claset));
   31.83 +by (safe_tac (claset()));
   31.84  by (stac expand_if 1);
   31.85   by (rtac conjI 1);
   31.86   by (rtac impI 1);
   31.87 @@ -132,7 +132,7 @@
   31.88  by (forward_tac  [reachable_rename] 1);
   31.89  by (Asm_full_simp_tac 1);
   31.90  (* x is internal *)
   31.91 -by (simp_tac (!simpset addcongs [conj_cong]) 1);
   31.92 +by (simp_tac (simpset() addcongs [conj_cong]) 1);
   31.93  by (rtac impI 1);
   31.94  by (etac conjE 1);
   31.95  by (forward_tac  [reachable_rename] 1);
    32.1 --- a/src/HOLCF/IOA/meta_theory/Seq.ML	Mon Nov 03 12:36:48 1997 +0100
    32.2 +++ b/src/HOLCF/IOA/meta_theory/Seq.ML	Mon Nov 03 14:06:27 1997 +0100
    32.3 @@ -357,32 +357,32 @@
    32.4  by (Simp_tac 1);
    32.5  by (Simp_tac 1);
    32.6  (* main case *)
    32.7 -by (asm_full_simp_tac (!simpset setloop split_If_tac) 1);
    32.8 +by (asm_full_simp_tac (simpset() setloop split_If_tac) 1);
    32.9  qed"sfiltersconc";
   32.10  
   32.11  goal thy "sforall P (stakewhile`P`x)";
   32.12 -by (simp_tac (!simpset addsimps [sforall_def]) 1);
   32.13 +by (simp_tac (simpset() addsimps [sforall_def]) 1);
   32.14  by (res_inst_tac[("x","x")] seq.ind 1);
   32.15  (* adm *)
   32.16 -by (simp_tac (!simpset addsimps [adm_trick_1]) 1);
   32.17 +by (simp_tac (simpset() addsimps [adm_trick_1]) 1);
   32.18  (* base cases *)
   32.19  by (Simp_tac 1);
   32.20  by (Simp_tac 1);
   32.21  (* main case *)
   32.22 -by (asm_full_simp_tac (!simpset setloop split_If_tac) 1);
   32.23 +by (asm_full_simp_tac (simpset() setloop split_If_tac) 1);
   32.24  qed"sforallPstakewhileP";
   32.25  
   32.26  goal thy "sforall P (sfilter`P`x)";
   32.27 -by (simp_tac (!simpset addsimps [sforall_def]) 1);
   32.28 +by (simp_tac (simpset() addsimps [sforall_def]) 1);
   32.29  by (res_inst_tac[("x","x")] seq.ind 1);
   32.30  (* adm *)
   32.31  (* FIX should be refined in _one_ tactic *)
   32.32 -by (simp_tac (!simpset addsimps [adm_trick_1]) 1);
   32.33 +by (simp_tac (simpset() addsimps [adm_trick_1]) 1);
   32.34  (* base cases *)
   32.35  by (Simp_tac 1);
   32.36  by (Simp_tac 1);
   32.37  (* main case *)
   32.38 -by (asm_full_simp_tac (!simpset setloop split_If_tac) 1);
   32.39 +by (asm_full_simp_tac (simpset() setloop split_If_tac) 1);
   32.40  qed"forallPsfilterP";
   32.41  
   32.42  
   32.43 @@ -413,7 +413,7 @@
   32.44  goal thy "Finite x --> a~=UU --> x=a##xs --> Finite xs";
   32.45  by (strip_tac 1);
   32.46  by (etac sfinite.elim 1);
   32.47 -by (fast_tac (HOL_cs addss !simpset) 1);
   32.48 +by (fast_tac (HOL_cs addss simpset()) 1);
   32.49  by (fast_tac (HOL_cs addSDs seq.injects) 1);
   32.50  qed"Finite_cons_a";
   32.51  
   32.52 @@ -471,13 +471,13 @@
   32.53     ------------------------------------------------------------------ *)
   32.54  
   32.55  goal thy "seq_finite nil";
   32.56 -by (simp_tac (!simpset addsimps [seq.sfinite_def]) 1);
   32.57 +by (simp_tac (simpset() addsimps [seq.sfinite_def]) 1);
   32.58  by (res_inst_tac [("x","Suc 0")] exI 1);
   32.59 -by (simp_tac (!simpset addsimps seq.rews) 1);
   32.60 +by (simp_tac (simpset() addsimps seq.rews) 1);
   32.61  qed"seq_finite_nil";
   32.62  
   32.63  goal thy "seq_finite UU";
   32.64 -by (simp_tac (!simpset addsimps [seq.sfinite_def]) 1);
   32.65 +by (simp_tac (simpset() addsimps [seq.sfinite_def]) 1);
   32.66  qed"seq_finite_UU";
   32.67  
   32.68  Addsimps[seq_finite_nil,seq_finite_UU];
   32.69 @@ -494,9 +494,9 @@
   32.70  by (rtac (logic_lemma RS mp RS mp) 1);
   32.71  by (rtac trf_impl_tf 1);
   32.72  by (rtac seq_finite_ind 1);
   32.73 -by (simp_tac (!simpset addsimps [Finite_def]) 1);
   32.74 -by (simp_tac (!simpset addsimps [Finite_def]) 1);
   32.75 -by (asm_full_simp_tac (!simpset addsimps [Finite_def]) 1);
   32.76 +by (simp_tac (simpset() addsimps [Finite_def]) 1);
   32.77 +by (simp_tac (simpset() addsimps [Finite_def]) 1);
   32.78 +by (asm_full_simp_tac (simpset() addsimps [Finite_def]) 1);
   32.79  qed"Finite_ind";
   32.80  
   32.81  
   32.82 @@ -505,17 +505,17 @@
   32.83  (* adm *)
   32.84  (* hier grosses Problem !!!!!!!!!!!!!!! *)
   32.85  
   32.86 -by (simp_tac (!simpset addsimps [Finite_def]) 2);
   32.87 -by (simp_tac (!simpset addsimps [Finite_def]) 2);
   32.88 +by (simp_tac (simpset() addsimps [Finite_def]) 2);
   32.89 +by (simp_tac (simpset() addsimps [Finite_def]) 2);
   32.90  
   32.91  (* main case *)
   32.92 -by (asm_full_simp_tac (!simpset addsimps [Finite_def,seq.sfinite_def]) 2);
   32.93 +by (asm_full_simp_tac (simpset() addsimps [Finite_def,seq.sfinite_def]) 2);
   32.94  by (rtac impI 2);
   32.95  by (rotate_tac 2 2);
   32.96  by (Asm_full_simp_tac 2);
   32.97  by (etac exE 2);
   32.98  by (res_inst_tac [("x","Suc n")] exI 2);
   32.99 -by (asm_full_simp_tac (!simpset addsimps seq.rews) 2);
  32.100 +by (asm_full_simp_tac (simpset() addsimps seq.rews) 2);
  32.101  qed"tf_is_trf";
  32.102  
  32.103  *)
    33.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Mon Nov 03 12:36:48 1997 +0100
    33.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Mon Nov 03 14:06:27 1997 +0100
    33.3 @@ -19,15 +19,15 @@
    33.4  (* ---------------------------------------------------------------- *)
    33.5  
    33.6  goal thy "Map f`UU =UU";
    33.7 -by (simp_tac (!simpset addsimps [Map_def]) 1);
    33.8 +by (simp_tac (simpset() addsimps [Map_def]) 1);
    33.9  qed"Map_UU";
   33.10  
   33.11  goal thy "Map f`nil =nil";
   33.12 -by (simp_tac (!simpset addsimps [Map_def]) 1);
   33.13 +by (simp_tac (simpset() addsimps [Map_def]) 1);
   33.14  qed"Map_nil";
   33.15  
   33.16  goal thy "Map f`(x>>xs)=(f x) >> Map f`xs";
   33.17 -by (simp_tac (!simpset addsimps [Map_def, Cons_def,flift2_def]) 1);
   33.18 +by (simp_tac (simpset() addsimps [Map_def, Cons_def,flift2_def]) 1);
   33.19  qed"Map_cons";
   33.20  
   33.21  (* ---------------------------------------------------------------- *)
   33.22 @@ -35,15 +35,15 @@
   33.23  (* ---------------------------------------------------------------- *)
   33.24  
   33.25  goal thy "Filter P`UU =UU";
   33.26 -by (simp_tac (!simpset addsimps [Filter_def]) 1);
   33.27 +by (simp_tac (simpset() addsimps [Filter_def]) 1);
   33.28  qed"Filter_UU";
   33.29  
   33.30  goal thy "Filter P`nil =nil";
   33.31 -by (simp_tac (!simpset addsimps [Filter_def]) 1);
   33.32 +by (simp_tac (simpset() addsimps [Filter_def]) 1);
   33.33  qed"Filter_nil";
   33.34  
   33.35  goal thy "Filter P`(x>>xs)= (if P x then x>>(Filter P`xs) else Filter P`xs)"; 
   33.36 -by (simp_tac (!simpset addsimps [Filter_def, Cons_def,flift2_def,If_and_if]) 1);
   33.37 +by (simp_tac (simpset() addsimps [Filter_def, Cons_def,flift2_def,If_and_if]) 1);
   33.38  qed"Filter_cons";
   33.39  
   33.40  (* ---------------------------------------------------------------- *)
   33.41 @@ -51,15 +51,15 @@
   33.42  (* ---------------------------------------------------------------- *)
   33.43  
   33.44  goal thy "Forall P UU";
   33.45 -by (simp_tac (!simpset addsimps [Forall_def,sforall_def]) 1);
   33.46 +by (simp_tac (simpset() addsimps [Forall_def,sforall_def]) 1);
   33.47  qed"Forall_UU";
   33.48  
   33.49  goal thy "Forall P nil";
   33.50 -by (simp_tac (!simpset addsimps [Forall_def,sforall_def]) 1);
   33.51 +by (simp_tac (simpset() addsimps [Forall_def,sforall_def]) 1);
   33.52  qed"Forall_nil";
   33.53  
   33.54  goal thy "Forall P (x>>xs)= (P x & Forall P xs)";
   33.55 -by (simp_tac (!simpset addsimps [Forall_def, sforall_def,
   33.56 +by (simp_tac (simpset() addsimps [Forall_def, sforall_def,
   33.57                                   Cons_def,flift2_def]) 1);
   33.58  qed"Forall_cons";
   33.59  
   33.60 @@ -69,7 +69,7 @@
   33.61  
   33.62  
   33.63  goal thy "(x>>xs) @@ y = x>>(xs @@y)"; 
   33.64 -by (simp_tac (!simpset addsimps [Cons_def]) 1);
   33.65 +by (simp_tac (simpset() addsimps [Cons_def]) 1);
   33.66  qed"Conc_cons";
   33.67  
   33.68  (* ---------------------------------------------------------------- *)
   33.69 @@ -77,15 +77,15 @@
   33.70  (* ---------------------------------------------------------------- *)
   33.71  
   33.72  goal thy "Takewhile P`UU =UU";
   33.73 -by (simp_tac (!simpset addsimps [Takewhile_def]) 1);
   33.74 +by (simp_tac (simpset() addsimps [Takewhile_def]) 1);
   33.75  qed"Takewhile_UU";
   33.76  
   33.77  goal thy "Takewhile P`nil =nil";
   33.78 -by (simp_tac (!simpset addsimps [Takewhile_def]) 1);
   33.79 +by (simp_tac (simpset() addsimps [Takewhile_def]) 1);
   33.80  qed"Takewhile_nil";
   33.81  
   33.82  goal thy "Takewhile P`(x>>xs)= (if P x then x>>(Takewhile P`xs) else nil)"; 
   33.83 -by (simp_tac (!simpset addsimps [Takewhile_def, Cons_def,flift2_def,If_and_if]) 1);
   33.84 +by (simp_tac (simpset() addsimps [Takewhile_def, Cons_def,flift2_def,If_and_if]) 1);
   33.85  qed"Takewhile_cons";
   33.86  
   33.87  (* ---------------------------------------------------------------- *)
   33.88 @@ -93,15 +93,15 @@
   33.89  (* ---------------------------------------------------------------- *)
   33.90  
   33.91  goal thy "Dropwhile P`UU =UU";
   33.92 -by (simp_tac (!simpset addsimps [Dropwhile_def]) 1);
   33.93 +by (simp_tac (simpset() addsimps [Dropwhile_def]) 1);
   33.94  qed"Dropwhile_UU";
   33.95  
   33.96  goal thy "Dropwhile P`nil =nil";
   33.97 -by (simp_tac (!simpset addsimps [Dropwhile_def]) 1);
   33.98 +by (simp_tac (simpset() addsimps [Dropwhile_def]) 1);
   33.99  qed"Dropwhile_nil";
  33.100  
  33.101  goal thy "Dropwhile P`(x>>xs)= (if P x then Dropwhile P`xs else x>>xs)"; 
  33.102 -by (simp_tac (!simpset addsimps [Dropwhile_def, Cons_def,flift2_def,If_and_if]) 1);
  33.103 +by (simp_tac (simpset() addsimps [Dropwhile_def, Cons_def,flift2_def,If_and_if]) 1);
  33.104  qed"Dropwhile_cons";
  33.105  
  33.106  (* ---------------------------------------------------------------- *)
  33.107 @@ -110,17 +110,17 @@
  33.108  
  33.109  
  33.110  goal thy "Last`UU =UU";
  33.111 -by (simp_tac (!simpset addsimps [Last_def]) 1);
  33.112 +by (simp_tac (simpset() addsimps [Last_def]) 1);
  33.113  qed"Last_UU";
  33.114  
  33.115  goal thy "Last`nil =UU";
  33.116 -by (simp_tac (!simpset addsimps [Last_def]) 1);
  33.117 +by (simp_tac (simpset() addsimps [Last_def]) 1);
  33.118  qed"Last_nil";
  33.119  
  33.120  goal thy "Last`(x>>xs)= (if xs=nil then Def x else Last`xs)"; 
  33.121 -by (simp_tac (!simpset addsimps [Last_def, Cons_def]) 1);
  33.122 +by (simp_tac (simpset() addsimps [Last_def, Cons_def]) 1);
  33.123  by (res_inst_tac [("x","xs")] seq.casedist 1);
  33.124 -by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
  33.125 +by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
  33.126  by (REPEAT (Asm_simp_tac 1));
  33.127  qed"Last_cons";
  33.128  
  33.129 @@ -130,15 +130,15 @@
  33.130  (* ---------------------------------------------------------------- *)
  33.131  
  33.132  goal thy "Flat`UU =UU";
  33.133 -by (simp_tac (!simpset addsimps [Flat_def]) 1);
  33.134 +by (simp_tac (simpset() addsimps [Flat_def]) 1);
  33.135  qed"Flat_UU";
  33.136  
  33.137  goal thy "Flat`nil =nil";
  33.138 -by (simp_tac (!simpset addsimps [Flat_def]) 1);
  33.139 +by (simp_tac (simpset() addsimps [Flat_def]) 1);
  33.140  qed"Flat_nil";
  33.141  
  33.142  goal thy "Flat`(x##xs)= x @@ (Flat`xs)"; 
  33.143 -by (simp_tac (!simpset addsimps [Flat_def, Cons_def]) 1);
  33.144 +by (simp_tac (simpset() addsimps [Flat_def, Cons_def]) 1);
  33.145  qed"Flat_cons";
  33.146  
  33.147  
  33.148 @@ -181,7 +181,7 @@
  33.149  
  33.150  goal thy "Zip`(x>>xs)`nil= UU"; 
  33.151  by (stac Zip_unfold 1);
  33.152 -by (simp_tac (!simpset addsimps [Cons_def]) 1);
  33.153 +by (simp_tac (simpset() addsimps [Cons_def]) 1);
  33.154  qed"Zip_cons_nil";
  33.155  
  33.156  goal thy "Zip`(x>>xs)`(y>>ys)= (x,y) >> Zip`xs`ys"; 
  33.157 @@ -190,7 +190,7 @@
  33.158  by (Simp_tac 1);
  33.159  (* FIX: Why Simp_tac 2 times. Does continuity in simpflication make job sometimes not 
  33.160    completely ready ? *)
  33.161 -by (simp_tac (!simpset addsimps [Cons_def]) 1);
  33.162 +by (simp_tac (simpset() addsimps [Cons_def]) 1);
  33.163  qed"Zip_cons";
  33.164  
  33.165  
  33.166 @@ -240,11 +240,11 @@
  33.167  section "Cons";
  33.168  
  33.169  goal thy "a>>s = (Def a)##s";
  33.170 -by (simp_tac (!simpset addsimps [Cons_def]) 1);
  33.171 +by (simp_tac (simpset() addsimps [Cons_def]) 1);
  33.172  qed"Cons_def2";
  33.173  
  33.174  goal thy "x = UU | x = nil | (? a s. x = a >> s)";
  33.175 -by (simp_tac (!simpset addsimps [Cons_def2]) 1);
  33.176 +by (simp_tac (simpset() addsimps [Cons_def2]) 1);
  33.177  by (cut_facts_tac [seq.exhaust] 1);
  33.178  by (fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1]) 1);
  33.179  qed"Seq_exhaust";
  33.180 @@ -279,7 +279,7 @@
  33.181  by (rtac notI 1);
  33.182  by (dtac antisym_less 1);
  33.183  by (Simp_tac 1);
  33.184 -by (asm_full_simp_tac (!simpset addsimps [Cons_not_UU]) 1);
  33.185 +by (asm_full_simp_tac (simpset() addsimps [Cons_not_UU]) 1);
  33.186  qed"Cons_not_less_UU";
  33.187  
  33.188  goal thy "~a>>s << nil";
  33.189 @@ -294,7 +294,7 @@
  33.190  qed"Cons_not_nil";
  33.191  
  33.192  goal thy "nil ~= a>>s";
  33.193 -by (simp_tac (!simpset addsimps [Cons_def2]) 1);
  33.194 +by (simp_tac (simpset() addsimps [Cons_def2]) 1);
  33.195  qed"Cons_not_nil2";
  33.196  
  33.197  goal thy "(a>>s = b>>t) = (a = b & s = t)";
  33.198 @@ -306,7 +306,7 @@
  33.199  qed"Cons_inject_eq";
  33.200  
  33.201  goal thy "(a>>s<<b>>t) = (a = b & s<<t)";
  33.202 -by (simp_tac (!simpset addsimps [Cons_def2]) 1);
  33.203 +by (simp_tac (simpset() addsimps [Cons_def2]) 1);
  33.204  by (stac (Def_inject_less_eq RS sym) 1);
  33.205  back();
  33.206  by (rtac iffI 1);
  33.207 @@ -320,7 +320,7 @@
  33.208  qed"Cons_inject_less_eq";
  33.209  
  33.210  goal thy "seq_take (Suc n)`(a>>x) = a>> (seq_take n`x)";
  33.211 -by (simp_tac (!simpset addsimps [Cons_def]) 1);
  33.212 +by (simp_tac (simpset() addsimps [Cons_def]) 1);
  33.213  qed"seq_take_Cons";
  33.214  
  33.215  Addsimps [Cons_not_nil2,Cons_inject_eq,Cons_inject_less_eq,seq_take_Cons,
  33.216 @@ -343,7 +343,7 @@
  33.217  by (etac seq.ind 1);
  33.218  by (REPEAT (atac 1));
  33.219  by (def_tac 1);
  33.220 -by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
  33.221 +by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
  33.222  qed"Seq_induct";
  33.223  
  33.224  goal thy "!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |]  \
  33.225 @@ -351,21 +351,21 @@
  33.226  by (etac seq_finite_ind 1);
  33.227  by (REPEAT (atac 1));
  33.228  by (def_tac 1);
  33.229 -by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
  33.230 +by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
  33.231  qed"Seq_FinitePartial_ind";
  33.232  
  33.233  goal thy "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x";
  33.234  by (etac sfinite.induct 1);
  33.235  by (assume_tac 1);
  33.236  by (def_tac 1);
  33.237 -by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
  33.238 +by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
  33.239  qed"Seq_Finite_ind"; 
  33.240  
  33.241  
  33.242  (* rws are definitions to be unfolded for admissibility check *)
  33.243  fun Seq_induct_tac s rws i = res_inst_tac [("x",s)] Seq_induct i
  33.244                           THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac (i+1))))
  33.245 -                         THEN simp_tac (!simpset addsimps rws) i;
  33.246 +                         THEN simp_tac (simpset() addsimps rws) i;
  33.247  
  33.248  fun Seq_Finite_induct_tac i = etac Seq_Finite_ind i
  33.249                                THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac i)));
  33.250 @@ -378,7 +378,7 @@
  33.251             res_inst_tac [("x",s)] Seq_induct i 
  33.252             THEN pair_tac "a" (i+3) 
  33.253             THEN (REPEAT_DETERM (CHANGED (Simp_tac (i+1)))) 
  33.254 -           THEN simp_tac (!simpset addsimps rws) i;
  33.255 +           THEN simp_tac (simpset() addsimps rws) i;
  33.256  
  33.257  
  33.258  
  33.259 @@ -387,11 +387,11 @@
  33.260  section "HD,TL";
  33.261  
  33.262  goal thy "HD`(x>>y) = Def x";
  33.263 -by (simp_tac (!simpset addsimps [Cons_def]) 1);
  33.264 +by (simp_tac (simpset() addsimps [Cons_def]) 1);
  33.265  qed"HD_Cons";
  33.266  
  33.267  goal thy "TL`(x>>y) = y";
  33.268 -by (simp_tac (!simpset addsimps [Cons_def]) 1);
  33.269 +by (simp_tac (simpset() addsimps [Cons_def]) 1);
  33.270  qed"TL_Cons";
  33.271  
  33.272  Addsimps [HD_Cons,TL_Cons];
  33.273 @@ -401,7 +401,7 @@
  33.274  section "Finite, Partial, Infinite";
  33.275  
  33.276  goal thy "Finite (a>>xs) = Finite xs";
  33.277 -by (simp_tac (!simpset addsimps [Cons_def2,Finite_cons]) 1);
  33.278 +by (simp_tac (simpset() addsimps [Cons_def2,Finite_cons]) 1);
  33.279  qed"Finite_Cons";
  33.280  
  33.281  Addsimps [Finite_Cons];
  33.282 @@ -421,7 +421,7 @@
  33.283  by (strip_tac 1);
  33.284  by (Seq_case_simp_tac "x" 1);
  33.285  by (Seq_case_simp_tac "y" 1);
  33.286 -by (SELECT_GOAL (auto_tac (!claset,!simpset))1);
  33.287 +by (SELECT_GOAL (auto_tac (claset(),simpset()))1);
  33.288  by (eres_inst_tac [("x","sa")] allE 1);
  33.289  by (eres_inst_tac [("x","y")] allE 1);
  33.290  by (Asm_full_simp_tac 1);
  33.291 @@ -463,7 +463,7 @@
  33.292  
  33.293  goal thy "!! s. Finite s ==> Finite (Filter P`s)";
  33.294  by (Seq_Finite_induct_tac 1);
  33.295 -by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
  33.296 +by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
  33.297  qed"FiniteFilter";
  33.298  
  33.299  
  33.300 @@ -545,12 +545,12 @@
  33.301  
  33.302  goal thy "!! s. Finite s ==> s~=nil --> Last`s~=UU";
  33.303  by (Seq_Finite_induct_tac  1);
  33.304 -by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
  33.305 +by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
  33.306  qed"Finite_Last1";
  33.307  
  33.308  goal thy "!! s. Finite s ==> Last`s=UU --> s=nil";
  33.309  by (Seq_Finite_induct_tac  1);
  33.310 -by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
  33.311 +by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
  33.312  by (fast_tac HOL_cs 1);
  33.313  qed"Finite_Last2";
  33.314  
  33.315 @@ -563,11 +563,11 @@
  33.316  
  33.317  goal thy "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
  33.318  by (Seq_induct_tac "s" [Filter_def] 1);
  33.319 -by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
  33.320 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
  33.321  qed"FilterPQ";
  33.322  
  33.323  goal thy "Filter P`(x @@ y) = (Filter P`x @@ Filter P`y)";
  33.324 -by (simp_tac (!simpset addsimps [Filter_def,sfiltersconc]) 1);
  33.325 +by (simp_tac (simpset() addsimps [Filter_def,sfiltersconc]) 1);
  33.326  qed"FilterConc";
  33.327  
  33.328  (* ------------------------------------------------------------------------------------ *)
  33.329 @@ -584,7 +584,7 @@
  33.330  
  33.331  goal thy "Filter P`(Map f`x) = Map f`(Filter (P o f)`x)";
  33.332  by (Seq_induct_tac "x" [] 1);
  33.333 -by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
  33.334 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
  33.335  qed"MapFilter";
  33.336  
  33.337  goal thy "nil = (Map f`s) --> s= nil";
  33.338 @@ -629,7 +629,7 @@
  33.339  
  33.340  goal thy "Forall P s  --> Forall P (Dropwhile Q`s)";
  33.341  by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
  33.342 -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  33.343 +by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
  33.344  qed"ForallDropwhile1";
  33.345  
  33.346  bind_thm ("ForallDropwhile",ForallDropwhile1 RS mp);
  33.347 @@ -666,7 +666,7 @@
  33.348  
  33.349  
  33.350  goal thy "Forall P (Filter P`x)";
  33.351 -by (simp_tac (!simpset addsimps [Filter_def,Forall_def,forallPsfilterP]) 1);
  33.352 +by (simp_tac (simpset() addsimps [Filter_def,Forall_def,forallPsfilterP]) 1);
  33.353  qed"ForallPFilterP";
  33.354  
  33.355  (* holds also in other direction, then equal to forallPfilterP *)
  33.356 @@ -707,7 +707,7 @@
  33.357  by (Simp_tac 1);
  33.358  by (Simp_tac 1);
  33.359  (* main case *)
  33.360 -by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
  33.361 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
  33.362  qed"FilternPnilForallP1";
  33.363  
  33.364  bind_thm ("FilternPnilForallP",FilternPnilForallP1 RS mp);
  33.365 @@ -716,12 +716,12 @@
  33.366  
  33.367  goal thy "!! ys. Finite ys ==> Filter P`ys ~= UU";
  33.368  by (Seq_Finite_induct_tac 1);
  33.369 -by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
  33.370 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
  33.371  qed"FilterUU_nFinite_lemma1";
  33.372  
  33.373  goal thy "~ Forall (%x. ~P x) ys --> Filter P`ys ~= UU";
  33.374  by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
  33.375 -by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
  33.376 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
  33.377  qed"FilterUU_nFinite_lemma2";
  33.378  
  33.379  goal thy   "!! P. Filter P`ys = UU ==> \
  33.380 @@ -729,7 +729,7 @@
  33.381  by (rtac conjI 1);
  33.382  by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1);
  33.383  by (Auto_tac());
  33.384 -by (blast_tac (!claset addSDs [FilterUU_nFinite_lemma1]) 1);
  33.385 +by (blast_tac (claset() addSDs [FilterUU_nFinite_lemma1]) 1);
  33.386  qed"FilternPUUForallP";
  33.387  
  33.388  
  33.389 @@ -755,7 +755,7 @@
  33.390  
  33.391  
  33.392  goal thy "Forall P (Takewhile P`x)";
  33.393 -by (simp_tac (!simpset addsimps [Forall_def,Takewhile_def,sforallPstakewhileP]) 1);
  33.394 +by (simp_tac (simpset() addsimps [Forall_def,Takewhile_def,sforallPstakewhileP]) 1);
  33.395  qed"ForallPTakewhileP";
  33.396  
  33.397  
  33.398 @@ -787,7 +787,7 @@
  33.399  
  33.400  goal thy "Takewhile P`(Takewhile P`s) = Takewhile P`s";
  33.401  by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
  33.402 -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  33.403 +by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
  33.404  qed"Takewhile_idempotent";
  33.405  
  33.406  goal thy "Forall P s --> Takewhile (%x. Q x | (~P x))`s = Takewhile Q`s";
  33.407 @@ -903,7 +903,7 @@
  33.408  goal thy "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 = seq_take k`y2|] \
  33.409  \ ==> seq_take n`(x @@ (s>>y1)) =  seq_take n`(y @@ (t>>y2))";
  33.410  
  33.411 -by (auto_tac (!claset addSIs [take_reduction1 RS spec RS mp],!simpset));
  33.412 +by (auto_tac (claset() addSIs [take_reduction1 RS spec RS mp],simpset()));
  33.413  qed"take_reduction";
  33.414  
  33.415  (* ------------------------------------------------------------------
  33.416 @@ -924,7 +924,7 @@
  33.417  
  33.418  goal thy "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 << seq_take k`y2|] \
  33.419  \ ==> seq_take n`(x @@ (s>>y1)) <<  seq_take n`(y @@ (t>>y2))";
  33.420 -by (auto_tac (!claset addSIs [take_reduction_less1 RS spec RS mp],!simpset));
  33.421 +by (auto_tac (claset() addSIs [take_reduction_less1 RS spec RS mp],simpset()));
  33.422  qed"take_reduction_less";
  33.423  
  33.424  
  33.425 @@ -962,7 +962,7 @@
  33.426  \                         ==> (f (s1 @@ y>>s2)) = (g (s1 @@ y>>s2)) |] \
  33.427  \              ==> A x --> (f x)=(g x)";
  33.428  by (case_tac "Forall Q x" 1);
  33.429 -by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
  33.430 +by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
  33.431  qed"take_lemma_principle1";
  33.432  
  33.433  goal thy "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
  33.434 @@ -971,7 +971,7 @@
  33.435  \                                = seq_take n`(g (s1 @@ y>>s2)) |] \
  33.436  \              ==> A x --> (f x)=(g x)";
  33.437  by (case_tac "Forall Q x" 1);
  33.438 -by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
  33.439 +by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
  33.440  by (resolve_tac seq.take_lemmas 1);
  33.441  by (Auto_tac());
  33.442  qed"take_lemma_principle2";
  33.443 @@ -1001,9 +1001,9 @@
  33.444  by (Simp_tac 1);
  33.445  by (rtac allI 1);
  33.446  by (case_tac "Forall Q xa" 1);
  33.447 -by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
  33.448 -                           !simpset)) 1);
  33.449 -by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
  33.450 +by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
  33.451 +                           simpset())) 1);
  33.452 +by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
  33.453  qed"take_lemma_induct";
  33.454  
  33.455  
  33.456 @@ -1022,9 +1022,9 @@
  33.457  by (rtac less_induct 1);
  33.458  by (rtac allI 1);
  33.459  by (case_tac "Forall Q xa" 1);
  33.460 -by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
  33.461 -                           !simpset)) 1);
  33.462 -by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
  33.463 +by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
  33.464 +                           simpset())) 1);
  33.465 +by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
  33.466  qed"take_lemma_less_induct";
  33.467  
  33.468  
  33.469 @@ -1076,9 +1076,9 @@
  33.470  by (rtac less_induct 1);
  33.471  by (rtac allI 1);
  33.472  by (case_tac "Forall Q xa" 1);
  33.473 -by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
  33.474 -                           !simpset)) 1);
  33.475 -by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
  33.476 +by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
  33.477 +                           simpset())) 1);
  33.478 +by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
  33.479  qed"take_lemma_less_induct";
  33.480  
  33.481  
  33.482 @@ -1103,9 +1103,9 @@
  33.483  by (rtac less_induct 1);
  33.484  by (rtac allI 1);
  33.485  by (case_tac "Forall Q xa" 1);
  33.486 -by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
  33.487 -                           !simpset)) 1);
  33.488 -by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
  33.489 +by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
  33.490 +                           simpset())) 1);
  33.491 +by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
  33.492  qed"take_lemma_less_induct";
  33.493  
  33.494  
  33.495 @@ -1151,21 +1151,21 @@
  33.496  \             Filter (%x. P x & Q x)`s";
  33.497  
  33.498  by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
  33.499 -by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
  33.500 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
  33.501  qed"Filter_lemma1";
  33.502  
  33.503  goal thy "!! s. Finite s ==>  \
  33.504  \         (Forall (%x. (~P x) | (~ Q x)) s  \
  33.505  \         --> Filter P`(Filter Q`s) = nil)";
  33.506  by (Seq_Finite_induct_tac 1);
  33.507 -by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
  33.508 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
  33.509  qed"Filter_lemma2";
  33.510  
  33.511  goal thy "!! s. Finite s ==>  \
  33.512  \         Forall (%x. (~P x) | (~ Q x)) s  \
  33.513  \         --> Filter (%x. P x & Q x)`s = nil";
  33.514  by (Seq_Finite_induct_tac 1);
  33.515 -by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
  33.516 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
  33.517  qed"Filter_lemma3";
  33.518  
  33.519  
  33.520 @@ -1175,8 +1175,8 @@
  33.521                   (take_lemma_induct RS mp) 1);
  33.522  (* FIX: better support for A = %x. True *)
  33.523  by (Fast_tac 3);
  33.524 -by (asm_full_simp_tac (!simpset addsimps [Filter_lemma1]) 1);
  33.525 -by (asm_full_simp_tac (!simpset addsimps [Filter_lemma2,Filter_lemma3] 
  33.526 +by (asm_full_simp_tac (simpset() addsimps [Filter_lemma1]) 1);
  33.527 +by (asm_full_simp_tac (simpset() addsimps [Filter_lemma2,Filter_lemma3] 
  33.528                                  setloop split_tac [expand_if]) 1);
  33.529  qed"FilterPQ_takelemma";
  33.530  
    34.1 --- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Mon Nov 03 12:36:48 1997 +0100
    34.2 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Mon Nov 03 14:06:27 1997 +0100
    34.3 @@ -49,8 +49,8 @@
    34.4  \          @@ (x>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`t))";     
    34.5  by (rtac trans 1);
    34.6  by (stac oraclebuild_unfold 1);
    34.7 -by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
    34.8 -by (simp_tac (!simpset addsimps [Cons_def]) 1);
    34.9 +by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
   34.10 +by (simp_tac (simpset() addsimps [Cons_def]) 1);
   34.11  qed"oraclebuild_cons";
   34.12  
   34.13  
   34.14 @@ -64,7 +64,7 @@
   34.15  "!! s. [| Forall (%a.~ P a) s; Finite s|] \
   34.16  \           ==> Cut P s =nil";
   34.17  by (subgoal_tac "Filter P`s = nil" 1);
   34.18 -by (asm_simp_tac (!simpset addsimps [oraclebuild_nil]) 1);
   34.19 +by (asm_simp_tac (simpset() addsimps [oraclebuild_nil]) 1);
   34.20  by (rtac ForallQFilterPnil 1);
   34.21  by (REPEAT (atac 1));
   34.22  qed"Cut_nil";
   34.23 @@ -73,7 +73,7 @@
   34.24  "!! s. [| Forall (%a.~ P a) s; ~Finite s|] \
   34.25  \           ==> Cut P s =UU";
   34.26  by (subgoal_tac "Filter P`s= UU" 1);
   34.27 -by (asm_simp_tac (!simpset addsimps [oraclebuild_UU]) 1);
   34.28 +by (asm_simp_tac (simpset() addsimps [oraclebuild_UU]) 1);
   34.29  by (rtac ForallQFilterPUU 1);
   34.30  by (REPEAT (atac 1));
   34.31  qed"Cut_UU";
   34.32 @@ -83,7 +83,7 @@
   34.33  \           ==> Cut P (ss @@ (t>> rs)) \
   34.34  \                = ss @@ (t >> Cut P rs)";
   34.35  
   34.36 -by (asm_full_simp_tac (!simpset addsimps [ForallQFilterPnil,oraclebuild_cons,
   34.37 +by (asm_full_simp_tac (simpset() addsimps [ForallQFilterPnil,oraclebuild_cons,
   34.38            TakewhileConc,DropwhileConc]) 1);
   34.39  qed"Cut_Cons";
   34.40  
   34.41 @@ -100,12 +100,12 @@
   34.42                   (take_lemma_induct RS mp) 1);
   34.43  by (Fast_tac 3);
   34.44  by (case_tac "Finite s" 1);
   34.45 -by (asm_full_simp_tac (!simpset addsimps [Cut_nil,
   34.46 +by (asm_full_simp_tac (simpset() addsimps [Cut_nil,
   34.47               ForallQFilterPnil]) 1);
   34.48 -by (asm_full_simp_tac (!simpset addsimps [Cut_UU,
   34.49 +by (asm_full_simp_tac (simpset() addsimps [Cut_UU,
   34.50               ForallQFilterPUU]) 1);
   34.51  (* main case *)
   34.52 -by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,ForallQFilterPnil]) 1);
   34.53 +by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,ForallQFilterPnil]) 1);
   34.54  by (Auto_tac());
   34.55  qed"FilterCut";
   34.56  
   34.57 @@ -117,12 +117,12 @@
   34.58                   (take_lemma_less_induct RS mp) 1);
   34.59  by (Fast_tac 3);
   34.60  by (case_tac "Finite s" 1);
   34.61 -by (asm_full_simp_tac (!simpset addsimps [Cut_nil,
   34.62 +by (asm_full_simp_tac (simpset() addsimps [Cut_nil,
   34.63               ForallQFilterPnil]) 1);
   34.64 -by (asm_full_simp_tac (!simpset addsimps [Cut_UU,
   34.65 +by (asm_full_simp_tac (simpset() addsimps [Cut_UU,
   34.66               ForallQFilterPUU]) 1);
   34.67  (* main case *)
   34.68 -by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,ForallQFilterPnil]) 1);
   34.69 +by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,ForallQFilterPnil]) 1);
   34.70  by (rtac take_reduction 1);
   34.71  by (Auto_tac());
   34.72  qed"Cut_idemp";
   34.73 @@ -135,17 +135,17 @@
   34.74                   (take_lemma_less_induct RS mp) 1);
   34.75  by (Fast_tac 3);
   34.76  by (case_tac "Finite s" 1);
   34.77 -by (asm_full_simp_tac (!simpset addsimps [Cut_nil]) 1); 
   34.78 +by (asm_full_simp_tac (simpset() addsimps [Cut_nil]) 1); 
   34.79  by (rtac (Cut_nil RS sym) 1);
   34.80 -by (asm_full_simp_tac (!simpset addsimps [ForallMap,o_def]) 1); 
   34.81 -by (asm_full_simp_tac (!simpset addsimps [Map2Finite]) 1);
   34.82 +by (asm_full_simp_tac (simpset() addsimps [ForallMap,o_def]) 1); 
   34.83 +by (asm_full_simp_tac (simpset() addsimps [Map2Finite]) 1);
   34.84  (* csae ~ Finite s *)
   34.85 -by (asm_full_simp_tac (!simpset addsimps [Cut_UU]) 1);
   34.86 +by (asm_full_simp_tac (simpset() addsimps [Cut_UU]) 1);
   34.87  by (rtac (Cut_UU RS sym) 1);
   34.88 -by (asm_full_simp_tac (!simpset addsimps [ForallMap,o_def]) 1); 
   34.89 -by (asm_full_simp_tac (!simpset addsimps [Map2Finite]) 1);
   34.90 +by (asm_full_simp_tac (simpset() addsimps [ForallMap,o_def]) 1); 
   34.91 +by (asm_full_simp_tac (simpset() addsimps [Map2Finite]) 1);
   34.92  (* main case *)
   34.93 -by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,MapConc,
   34.94 +by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,MapConc,
   34.95            ForallMap,FiniteMap1,o_def]) 1);
   34.96  by (rtac take_reduction 1);
   34.97  by (Auto_tac());
   34.98 @@ -165,13 +165,13 @@
   34.99  ren "na n s" 1;
  34.100  by (case_tac "Forall (%x. ~ P x) s" 1);
  34.101  by (rtac (take_lemma_less RS iffD2 RS spec) 1);
  34.102 -by (asm_full_simp_tac (!simpset addsimps [Cut_UU]) 1);
  34.103 +by (asm_full_simp_tac (simpset() addsimps [Cut_UU]) 1);
  34.104  (* main case *)
  34.105  by (dtac divide_Seq3 1);
  34.106  by (REPEAT (etac exE 1));
  34.107  by (REPEAT (etac conjE 1));
  34.108  by (hyp_subst_tac 1);
  34.109 -by (asm_full_simp_tac (!simpset addsimps [Cut_Cons]) 1);
  34.110 +by (asm_full_simp_tac (simpset() addsimps [Cut_Cons]) 1);
  34.111  by (rtac take_reduction_less 1);
  34.112  (* auto makes also reasoning about Finiteness of parts of s ! *)
  34.113  by (Auto_tac());
  34.114 @@ -194,13 +194,13 @@
  34.115  ren "na n s" 1;
  34.116  by (case_tac "Forall (%x. ~ P x) s" 1);
  34.117  by (rtac (seq_take_lemma RS iffD2 RS spec) 1);
  34.118 -by (asm_full_simp_tac (!simpset addsimps [Cut_nil]) 1);
  34.119 +by (asm_full_simp_tac (simpset() addsimps [Cut_nil]) 1);
  34.120  (* main case *)
  34.121  by (dtac divide_Seq3 1);
  34.122  by (REPEAT (etac exE 1));
  34.123  by (REPEAT (etac conjE 1));
  34.124  by (hyp_subst_tac 1);
  34.125 -by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,Conc_assoc]) 1);
  34.126 +by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,Conc_assoc]) 1);
  34.127  by (rtac take_reduction 1);
  34.128  
  34.129  qed_spec_mp"Cut_prefixcl_Finite";
  34.130 @@ -237,7 +237,7 @@
  34.131  
  34.132  by (safe_tac set_cs);
  34.133  by (res_inst_tac [("x","filter_act`(Cut (%a. fst a:ext A) (snd ex))")] exI 1);
  34.134 -by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
  34.135 +by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
  34.136  by (pair_tac "ex" 1);
  34.137  by (safe_tac set_cs);
  34.138  by (res_inst_tac [("x","(x,Cut (%a. fst a:ext A) y)")] exI 1);
  34.139 @@ -245,21 +245,21 @@
  34.140  
  34.141  (* Subgoal 1: Lemma:  propagation of execution through Cut *)
  34.142  
  34.143 -by (asm_full_simp_tac (!simpset addsimps [execThruCut]) 1);
  34.144 +by (asm_full_simp_tac (simpset() addsimps [execThruCut]) 1);
  34.145  
  34.146  (* Subgoal 2:  Lemma:  Filter P s = Filter P (Cut P s) *)
  34.147  
  34.148 -by (simp_tac (!simpset addsimps [filter_act_def]) 1);
  34.149 +by (simp_tac (simpset() addsimps [filter_act_def]) 1);
  34.150  by (subgoal_tac "Map fst`(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst`y)" 1);
  34.151  by (rtac (rewrite_rule [o_def] MapCut) 2);
  34.152 -by (asm_full_simp_tac (!simpset addsimps [FilterCut RS sym]) 1);
  34.153 +by (asm_full_simp_tac (simpset() addsimps [FilterCut RS sym]) 1);
  34.154  
  34.155  (* Subgoal 3: Lemma: Cut idempotent  *)
  34.156  
  34.157 -by (simp_tac (!simpset addsimps [LastActExtsch_def,filter_act_def]) 1);
  34.158 +by (simp_tac (simpset() addsimps [LastActExtsch_def,filter_act_def]) 1);
  34.159  by (subgoal_tac "Map fst`(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst`y)" 1);
  34.160  by (rtac (rewrite_rule [o_def] MapCut) 2);
  34.161 -by (asm_full_simp_tac (!simpset addsimps [Cut_idemp]) 1);
  34.162 +by (asm_full_simp_tac (simpset() addsimps [Cut_idemp]) 1);
  34.163  qed"exists_LastActExtsch";
  34.164  
  34.165  
    35.1 --- a/src/HOLCF/IOA/meta_theory/Traces.ML	Mon Nov 03 12:36:48 1997 +0100
    35.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Mon Nov 03 14:06:27 1997 +0100
    35.3 @@ -23,15 +23,15 @@
    35.4  
    35.5  
    35.6  goal thy  "filter_act`UU = UU";
    35.7 -by (simp_tac (!simpset addsimps [filter_act_def]) 1);
    35.8 +by (simp_tac (simpset() addsimps [filter_act_def]) 1);
    35.9  qed"filter_act_UU";
   35.10  
   35.11  goal thy  "filter_act`nil = nil";
   35.12 -by (simp_tac (!simpset addsimps [filter_act_def]) 1);
   35.13 +by (simp_tac (simpset() addsimps [filter_act_def]) 1);
   35.14  qed"filter_act_nil";
   35.15  
   35.16  goal thy "filter_act`(x>>xs) = (fst x) >> filter_act`xs";
   35.17 -by (simp_tac (!simpset addsimps [filter_act_def]) 1);
   35.18 +by (simp_tac (simpset() addsimps [filter_act_def]) 1);
   35.19  qed"filter_act_cons";
   35.20  
   35.21  Addsimps [filter_act_UU,filter_act_nil,filter_act_cons];
   35.22 @@ -42,11 +42,11 @@
   35.23  (* ---------------------------------------------------------------- *)
   35.24  
   35.25  goal thy "mk_trace A`UU=UU";
   35.26 -by (simp_tac (!simpset addsimps [mk_trace_def]) 1);
   35.27 +by (simp_tac (simpset() addsimps [mk_trace_def]) 1);
   35.28  qed"mk_trace_UU";
   35.29  
   35.30  goal thy "mk_trace A`nil=nil";
   35.31 -by (simp_tac (!simpset addsimps [mk_trace_def]) 1);
   35.32 +by (simp_tac (simpset() addsimps [mk_trace_def]) 1);
   35.33  qed"mk_trace_nil";
   35.34  
   35.35  goal thy "mk_trace A`(at >> xs) =    \
   35.36 @@ -54,7 +54,7 @@
   35.37  \                 then (fst at) >> (mk_trace A`xs) \   
   35.38  \                 else mk_trace A`xs)";
   35.39  
   35.40 -by (asm_full_simp_tac (!simpset addsimps [mk_trace_def]) 1);
   35.41 +by (asm_full_simp_tac (simpset() addsimps [mk_trace_def]) 1);
   35.42  qed"mk_trace_cons";
   35.43  
   35.44  Addsimps [mk_trace_UU,mk_trace_nil,mk_trace_cons];
   35.45 @@ -74,7 +74,7 @@
   35.46  by (rtac fix_eq2 1);
   35.47  by (rtac is_exec_fragC_def 1);
   35.48  by (rtac beta_cfun 1);
   35.49 -by (simp_tac (!simpset addsimps [flift1_def]) 1);
   35.50 +by (simp_tac (simpset() addsimps [flift1_def]) 1);
   35.51  qed"is_exec_fragC_unfold";
   35.52  
   35.53  goal thy "(is_exec_fragC A`UU) s=UU";
   35.54 @@ -92,7 +92,7 @@
   35.55  \                andalso (is_exec_fragC A`xs)(snd pr))";
   35.56  by (rtac trans 1);
   35.57  by (stac is_exec_fragC_unfold 1);
   35.58 -by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1);
   35.59 +by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
   35.60  by (Simp_tac 1);
   35.61  qed"is_exec_fragC_cons";
   35.62  
   35.63 @@ -105,17 +105,17 @@
   35.64  (* ---------------------------------------------------------------- *)
   35.65  
   35.66  goal thy "is_exec_frag A (s, UU)";
   35.67 -by (simp_tac (!simpset addsimps [is_exec_frag_def]) 1);
   35.68 +by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1);
   35.69  qed"is_exec_frag_UU";
   35.70  
   35.71  goal thy "is_exec_frag A (s, nil)";
   35.72 -by (simp_tac (!simpset addsimps [is_exec_frag_def]) 1);
   35.73 +by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1);
   35.74  qed"is_exec_frag_nil";
   35.75  
   35.76  goal thy "is_exec_frag A (s, (a,t)>>ex) = \
   35.77  \                               (((s,a,t):trans_of A) & \
   35.78  \                               is_exec_frag A (t, ex))";
   35.79 -by (simp_tac (!simpset addsimps [is_exec_frag_def]) 1);
   35.80 +by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1);
   35.81  qed"is_exec_frag_cons";
   35.82  
   35.83  
   35.84 @@ -169,14 +169,14 @@
   35.85  (* main case *)
   35.86  ren "ss a t" 1;
   35.87  by (safe_tac set_cs);
   35.88 -by (REPEAT (asm_full_simp_tac (!simpset addsimps [is_trans_of_def]) 1));
   35.89 +by (REPEAT (asm_full_simp_tac (simpset() addsimps [is_trans_of_def]) 1));
   35.90  qed"execfrag_in_sig";
   35.91  
   35.92  goal thy 
   35.93    "!! A.[|  is_trans_of A; x:executions A |] ==> \
   35.94  \ Forall (%a. a:act A) (filter_act`(snd x))";
   35.95  
   35.96 -by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
   35.97 +by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
   35.98  by (pair_tac "x" 1);
   35.99  by (rtac (execfrag_in_sig RS spec RS mp) 1);
  35.100  by (Auto_tac());
  35.101 @@ -186,7 +186,7 @@
  35.102    "!! A.[|  is_trans_of A; x:schedules A |] ==> \
  35.103  \   Forall (%a. a:act A) x";
  35.104  
  35.105 -by (fast_tac (!claset addSIs [exec_in_sig]) 1);
  35.106 +by (fast_tac (claset() addSIs [exec_in_sig]) 1);
  35.107  qed"scheds_in_sig";
  35.108  
  35.109  
    36.1 --- a/src/HOLCF/Lift.ML	Mon Nov 03 12:36:48 1997 +0100
    36.2 +++ b/src/HOLCF/Lift.ML	Mon Nov 03 14:06:27 1997 +0100
    36.3 @@ -28,7 +28,7 @@
    36.4  by (strip_tac 1);
    36.5  by (res_inst_tac [("x","y")] Lift_cases 1);
    36.6  by (Asm_simp_tac 1);
    36.7 -by (fast_tac (HOL_cs addss !simpset) 1);
    36.8 +by (fast_tac (HOL_cs addss simpset()) 1);
    36.9  qed"cont_flift1_not_arg";
   36.10  
   36.11  (* flift1 is continuous in a variable that occurs either 
   36.12 @@ -69,11 +69,11 @@
   36.13  fun cont_tac  i = resolve_tac cont_lemmas2 i;
   36.14  fun cont_tacR i = REPEAT (cont_tac i);
   36.15  
   36.16 -fun cont_tacRs i = simp_tac (!simpset addsimps [flift1_def,flift2_def]) i THEN
   36.17 +fun cont_tacRs i = simp_tac (simpset() addsimps [flift1_def,flift2_def]) i THEN
   36.18                    REPEAT (cont_tac i);
   36.19  
   36.20  
   36.21 -simpset := !simpset addSolver (K (DEPTH_SOLVE_1 o cont_tac));
   36.22 +simpset_ref() := simpset() addSolver (K (DEPTH_SOLVE_1 o cont_tac));
   36.23  
   36.24  
   36.25  
   36.26 @@ -83,19 +83,19 @@
   36.27  
   36.28  
   36.29  goal thy "flift1 f`(Def x) = (f x)";
   36.30 -by (simp_tac (!simpset addsimps [flift1_def]) 1);
   36.31 +by (simp_tac (simpset() addsimps [flift1_def]) 1);
   36.32  qed"flift1_Def";
   36.33  
   36.34  goal thy "flift2 f`(Def x) = Def (f x)";
   36.35 -by (simp_tac (!simpset addsimps [flift2_def]) 1);
   36.36 +by (simp_tac (simpset() addsimps [flift2_def]) 1);
   36.37  qed"flift2_Def";
   36.38  
   36.39  goal thy "flift1 f`UU = UU";
   36.40 -by (simp_tac (!simpset addsimps [flift1_def]) 1);
   36.41 +by (simp_tac (simpset() addsimps [flift1_def]) 1);
   36.42  qed"flift1_UU";
   36.43  
   36.44  goal thy "flift2 f`UU = UU";
   36.45 -by (simp_tac (!simpset addsimps [flift2_def]) 1);
   36.46 +by (simp_tac (simpset() addsimps [flift2_def]) 1);
   36.47  qed"flift2_UU";
   36.48  
   36.49  Addsimps [flift1_Def,flift2_Def,flift1_UU,flift2_UU];
    37.1 --- a/src/HOLCF/Lift2.ML	Mon Nov 03 12:36:48 1997 +0100
    37.2 +++ b/src/HOLCF/Lift2.ML	Mon Nov 03 14:06:27 1997 +0100
    37.3 @@ -21,7 +21,7 @@
    37.4  (* ------------------------------------------------------------------------ *)
    37.5  
    37.6  goal Lift2.thy  "Undef << x";
    37.7 -by (simp_tac (!simpset addsimps [inst_lift_po]) 1);
    37.8 +by (simp_tac (simpset() addsimps [inst_lift_po]) 1);
    37.9  qed"minimal_lift";
   37.10  
   37.11  bind_thm ("UU_lift_def",minimal_lift RS minimal2UU RS sym);
   37.12 @@ -83,7 +83,7 @@
   37.13  by (etac spec 1); 
   37.14  
   37.15  by (subgoal_tac "!x y. x<<(y::('a)lift) --> x=Undef | x=y" 1);
   37.16 -by (simp_tac (!simpset addsimps [inst_lift_po]) 2);
   37.17 +by (simp_tac (simpset() addsimps [inst_lift_po]) 2);
   37.18  by (rtac (chain_mono2_po RS exE) 1); 
   37.19  by (Fast_tac 1); 
   37.20  by (atac 1); 
    38.1 --- a/src/HOLCF/Lift3.ML	Mon Nov 03 12:36:48 1997 +0100
    38.2 +++ b/src/HOLCF/Lift3.ML	Mon Nov 03 14:06:27 1997 +0100
    38.3 @@ -25,7 +25,7 @@
    38.4  local
    38.5  
    38.6  val case1' = prove_goal thy "lift_case f1 f2 UU = f1"
    38.7 -             (fn _ => [simp_tac (!simpset addsimps lift.simps) 1]);
    38.8 +             (fn _ => [simp_tac (simpset() addsimps lift.simps) 1]);
    38.9  val case2' = prove_goal thy "lift_case f1 f2 (Def a) = f2 a"
   38.10               (fn _ => [Simp_tac 1]);
   38.11  val distinct1' = prove_goal thy "UU ~= Def a" 
   38.12 @@ -125,12 +125,12 @@
   38.13  by (stac (hd lift.inject RS sym) 1);
   38.14  back();
   38.15  by (rtac iffI 1);
   38.16 -by (asm_full_simp_tac (!simpset addsimps [inst_lift_po] ) 1);
   38.17 +by (asm_full_simp_tac (simpset() addsimps [inst_lift_po] ) 1);
   38.18  by (etac (antisym_less_inverse RS conjunct1) 1);
   38.19  qed"Def_inject_less_eq";
   38.20  
   38.21  goal thy "Def x << y = (Def x = y)";
   38.22 -by (simp_tac (!simpset addsimps [less_lift]) 1);
   38.23 +by (simp_tac (simpset() addsimps [less_lift]) 1);
   38.24  qed"Def_less_is_eq";
   38.25  
   38.26  Addsimps [Def_less_is_eq];
   38.27 @@ -140,7 +140,7 @@
   38.28  (* ---------------------------------------------------------- *)
   38.29  
   38.30  goal thy "! x y::'a lift. x << y --> x = UU | x = y";
   38.31 -by (simp_tac (!simpset addsimps [less_lift]) 1);
   38.32 +by (simp_tac (simpset() addsimps [less_lift]) 1);
   38.33  qed"ax_flat_lift";
   38.34  
   38.35  (* Two specific lemmas for the combination of LCF and HOL terms *)
    39.1 --- a/src/HOLCF/One.ML	Mon Nov 03 12:36:48 1997 +0100
    39.2 +++ b/src/HOLCF/One.ML	Mon Nov 03 14:06:27 1997 +0100
    39.3 @@ -37,7 +37,7 @@
    39.4  fun prover t = prove_goalw thy [ONE_def] t
    39.5   (fn prems =>
    39.6          [
    39.7 -	(asm_simp_tac (!simpset addsimps [inst_lift_po]) 1)
    39.8 +	(asm_simp_tac (simpset() addsimps [inst_lift_po]) 1)
    39.9  	]);
   39.10  
   39.11  (* ------------------------------------------------------------------------ *)
    40.1 --- a/src/HOLCF/Pcpo.ML	Mon Nov 03 12:36:48 1997 +0100
    40.2 +++ b/src/HOLCF/Pcpo.ML	Mon Nov 03 14:06:27 1997 +0100
    40.3 @@ -56,7 +56,7 @@
    40.4          safe_tac (HOL_cs addSIs [antisym_less]),
    40.5          fast_tac (HOL_cs addSEs [chain_mono3]) 1,
    40.6          dtac sym 1,
    40.7 -        fast_tac ((HOL_cs addSEs [is_ub_thelub]) addss !simpset) 1
    40.8 +        fast_tac ((HOL_cs addSEs [is_ub_thelub]) addss simpset()) 1
    40.9          ]);
   40.10  
   40.11  
   40.12 @@ -314,7 +314,7 @@
   40.13  	[
   40.14  	cut_facts_tac prems 1,
   40.15  	fast_tac (HOL_cs addss 
   40.16 -		 (!simpset addsimps [chfin,finite_chain_def])) 1
   40.17 +		 (simpset() addsimps [chfin,finite_chain_def])) 1
   40.18  	]);
   40.19  
   40.20  (* ------------------------------------------------------------------------ *)
    41.1 --- a/src/HOLCF/Porder.ML	Mon Nov 03 12:36:48 1997 +0100
    41.2 +++ b/src/HOLCF/Porder.ML	Mon Nov 03 14:06:27 1997 +0100
    41.3 @@ -70,7 +70,7 @@
    41.4          [
    41.5          Safe_tac,
    41.6          (rtac nat_less_cases 1),
    41.7 -        (ALLGOALS (fast_tac (!claset addIs [refl_less, chain_mono RS mp])))]);
    41.8 +        (ALLGOALS (fast_tac (claset() addIs [refl_less, chain_mono RS mp])))]);
    41.9  
   41.10  (* ------------------------------------------------------------------------ *)
   41.11  (* technical lemmas about lub and is_lub                                    *)
   41.12 @@ -114,7 +114,7 @@
   41.13  
   41.14  goal thy "lub{x} = x";
   41.15  by (rtac thelubI 1);
   41.16 -by (simp_tac (!simpset addsimps [is_lub,is_ub]) 1);
   41.17 +by (simp_tac (simpset() addsimps [is_lub,is_ub]) 1);
   41.18  qed "lub_singleton";
   41.19  Addsimps [lub_singleton];
   41.20  
    42.1 --- a/src/HOLCF/Sprod3.ML	Mon Nov 03 12:36:48 1997 +0100
    42.2 +++ b/src/HOLCF/Sprod3.ML	Mon Nov 03 14:06:27 1997 +0100
    42.3 @@ -319,7 +319,7 @@
    42.4   (fn prems =>
    42.5          [
    42.6          (stac beta_cfun 1),
    42.7 -        (simp_tac (!simpset addsimps [cont_Ispair2, cont_Ispair1,
    42.8 +        (simp_tac (simpset() addsimps [cont_Ispair2, cont_Ispair1,
    42.9  					cont2cont_CF1L]) 1),
   42.10          (stac beta_cfun 1),
   42.11          (rtac cont_Ispair2 1),
    43.1 --- a/src/HOLCF/Ssum0.ML	Mon Nov 03 12:36:48 1997 +0100
    43.2 +++ b/src/HOLCF/Ssum0.ML	Mon Nov 03 14:06:27 1997 +0100
    43.3 @@ -388,6 +388,6 @@
    43.4  (* instantiate the simplifier                                               *)
    43.5  (* ------------------------------------------------------------------------ *)
    43.6  
    43.7 -val Ssum0_ss = (simpset_of "Cfun3") addsimps 
    43.8 +val Ssum0_ss = (simpset_of Cfun3.thy) addsimps 
    43.9                  [(strict_IsinlIsinr RS sym),Iwhen1,Iwhen2,Iwhen3];
   43.10  
    44.1 --- a/src/HOLCF/Ssum2.ML	Mon Nov 03 12:36:48 1997 +0100
    44.2 +++ b/src/HOLCF/Ssum2.ML	Mon Nov 03 14:06:27 1997 +0100
    44.3 @@ -27,25 +27,25 @@
    44.4  qed_goal "less_ssum3a" thy "Isinl x << Isinl y = x << y"
    44.5   (fn prems =>
    44.6          [
    44.7 -        (simp_tac (!simpset addsimps [less_ssum2a]) 1)
    44.8 +        (simp_tac (simpset() addsimps [less_ssum2a]) 1)
    44.9          ]);
   44.10  
   44.11  qed_goal "less_ssum3b" thy "Isinr x << Isinr y = x << y"
   44.12   (fn prems =>
   44.13          [
   44.14 -        (simp_tac (!simpset addsimps [less_ssum2b]) 1)
   44.15 +        (simp_tac (simpset() addsimps [less_ssum2b]) 1)
   44.16          ]);
   44.17  
   44.18  qed_goal "less_ssum3c" thy "Isinl x << Isinr y = (x = UU)"
   44.19   (fn prems =>
   44.20          [
   44.21 -        (simp_tac (!simpset addsimps [less_ssum2c]) 1)
   44.22 +        (simp_tac (simpset() addsimps [less_ssum2c]) 1)
   44.23          ]);
   44.24  
   44.25  qed_goal "less_ssum3d" thy "Isinr x << Isinl y = (x = UU)"
   44.26   (fn prems =>
   44.27          [
   44.28 -        (simp_tac (!simpset addsimps [less_ssum2d]) 1)
   44.29 +        (simp_tac (simpset() addsimps [less_ssum2d]) 1)
   44.30          ]);
   44.31  
   44.32  (* ------------------------------------------------------------------------ *)
    45.1 --- a/src/HOLCF/Ssum3.ML	Mon Nov 03 12:36:48 1997 +0100
    45.2 +++ b/src/HOLCF/Ssum3.ML	Mon Nov 03 14:06:27 1997 +0100
    45.3 @@ -261,7 +261,7 @@
    45.4          (res_inst_tac [("t","Y(i)")] ssubst 1),
    45.5          (atac 1),
    45.6          (fast_tac HOL_cs 1),
    45.7 -        (simp_tac (simpset_of "Cfun3") 1),
    45.8 +        (simp_tac (simpset_of Cfun3.thy) 1),
    45.9          (rtac (monofun_fapp2 RS ch2ch_monofun) 1),
   45.10          (etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
   45.11          (etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
   45.12 @@ -325,7 +325,7 @@
   45.13          (res_inst_tac [("t","Y(i)")] ssubst 1),
   45.14          (atac 1),
   45.15          (fast_tac HOL_cs 1),
   45.16 -        (simp_tac (simpset_of "Cfun3") 1),
   45.17 +        (simp_tac (simpset_of Cfun3.thy) 1),
   45.18          (rtac (monofun_fapp2 RS ch2ch_monofun) 1),
   45.19          (etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
   45.20          (etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
   45.21 @@ -691,9 +691,9 @@
   45.22   (fn prems =>
   45.23          [
   45.24          (res_inst_tac [("p","z")] ssumE 1),
   45.25 -        (asm_simp_tac ((simpset_of "Cfun3") addsimps [sswhen1,sswhen2,sswhen3]) 1),
   45.26 -        (asm_simp_tac ((simpset_of "Cfun3") addsimps [sswhen1,sswhen2,sswhen3]) 1),
   45.27 -        (asm_simp_tac ((simpset_of "Cfun3") addsimps [sswhen1,sswhen2,sswhen3]) 1)
   45.28 +        (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sswhen1,sswhen2,sswhen3]) 1),
   45.29 +        (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sswhen1,sswhen2,sswhen3]) 1),
   45.30 +        (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sswhen1,sswhen2,sswhen3]) 1)
   45.31          ]);
   45.32  
   45.33  
    46.1 --- a/src/HOLCF/Tr.ML	Mon Nov 03 12:36:48 1997 +0100
    46.2 +++ b/src/HOLCF/Tr.ML	Mon Nov 03 14:06:27 1997 +0100
    46.3 @@ -16,7 +16,7 @@
    46.4          [
    46.5  	(lift.induct_tac "t" 1),
    46.6  	(fast_tac HOL_cs 1),
    46.7 -	(fast_tac (HOL_cs addss !simpset) 1)
    46.8 +	(fast_tac (HOL_cs addss simpset()) 1)
    46.9  	]);
   46.10  
   46.11  qed_goal "trE" thy
   46.12 @@ -40,7 +40,7 @@
   46.13   (fn prems =>
   46.14          [
   46.15          (res_inst_tac [("p","y")] trE 1),
   46.16 -	(REPEAT(asm_simp_tac (!simpset addsimps 
   46.17 +	(REPEAT(asm_simp_tac (simpset() addsimps 
   46.18  		[o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1))
   46.19  	]);
   46.20  
   46.21 @@ -129,28 +129,28 @@
   46.22  qed"andalso_and";
   46.23  
   46.24  goal thy "(Def x ~=FF)= x";
   46.25 -by (simp_tac (!simpset addsimps [FF_def]) 1);
   46.26 +by (simp_tac (simpset() addsimps [FF_def]) 1);
   46.27  qed"Def_bool1";
   46.28  
   46.29  goal thy "(Def x = FF) = (~x)";
   46.30 -by (simp_tac (!simpset addsimps [FF_def]) 1);
   46.31 +by (simp_tac (simpset() addsimps [FF_def]) 1);
   46.32  by (fast_tac HOL_cs 1);
   46.33  qed"Def_bool2";
   46.34  
   46.35  goal thy "(Def x = TT) = x";
   46.36 -by (simp_tac (!simpset addsimps [TT_def]) 1);
   46.37 +by (simp_tac (simpset() addsimps [TT_def]) 1);
   46.38  qed"Def_bool3";
   46.39  
   46.40  goal thy "(Def x ~= TT) = (~x)";
   46.41 -by (simp_tac (!simpset addsimps [TT_def]) 1);
   46.42 +by (simp_tac (simpset() addsimps [TT_def]) 1);
   46.43  qed"Def_bool4";
   46.44  
   46.45  goal thy 
   46.46    "(If Def P then A else B fi)= (if P then A else B)";
   46.47  by (res_inst_tac [("p","Def P")]  trE 1);
   46.48  by (Asm_full_simp_tac 1);
   46.49 -by (asm_full_simp_tac (!simpset addsimps tr_defs@[flift1_def,o_def]) 1);
   46.50 -by (asm_full_simp_tac (!simpset addsimps tr_defs@[flift1_def,o_def]) 1);
   46.51 +by (asm_full_simp_tac (simpset() addsimps tr_defs@[flift1_def,o_def]) 1);
   46.52 +by (asm_full_simp_tac (simpset() addsimps tr_defs@[flift1_def,o_def]) 1);
   46.53  qed"If_and_if";
   46.54  
   46.55  Addsimps [Def_bool1,Def_bool2,Def_bool3,Def_bool4];
    47.1 --- a/src/HOLCF/Up1.ML	Mon Nov 03 12:36:48 1997 +0100
    47.2 +++ b/src/HOLCF/Up1.ML	Mon Nov 03 14:06:27 1997 +0100
    47.3 @@ -9,7 +9,7 @@
    47.4  qed_goal "Abs_Up_inverse2" thy "Rep_Up (Abs_Up y) = y"
    47.5   (fn prems =>
    47.6          [
    47.7 -	(simp_tac (!simpset addsimps [Up_def,Abs_Up_inverse]) 1)
    47.8 +	(simp_tac (simpset() addsimps [Up_def,Abs_Up_inverse]) 1)
    47.9  	]);
   47.10  
   47.11  qed_goalw "Exh_Up" thy [Iup_def ]
   47.12 @@ -90,7 +90,7 @@
   47.13          (rtac refl 1)
   47.14          ]);
   47.15  
   47.16 -val Up0_ss = (simpset_of "Cfun3") addsimps [Ifup1,Ifup2];
   47.17 +val Up0_ss = (simpset_of Cfun3.thy) addsimps [Ifup1,Ifup2];
   47.18  
   47.19  qed_goalw "less_up1a"  thy [less_up_def]
   47.20          "Abs_Up(Inl ())<< z"
    48.1 --- a/src/HOLCF/Up2.ML	Mon Nov 03 12:36:48 1997 +0100
    48.2 +++ b/src/HOLCF/Up2.ML	Mon Nov 03 14:06:27 1997 +0100
    48.3 @@ -26,7 +26,7 @@
    48.4  qed_goal "minimal_up" thy "Abs_Up(Inl ()) << z"
    48.5   (fn prems =>
    48.6          [
    48.7 -        (simp_tac (!simpset addsimps [less_up1a]) 1)
    48.8 +        (simp_tac (simpset() addsimps [less_up1a]) 1)
    48.9          ]);
   48.10  
   48.11  bind_thm ("UU_up_def",minimal_up RS minimal2UU RS sym);
   48.12 @@ -45,13 +45,13 @@
   48.13  qed_goal "less_up2b" thy "~ Iup(x) << Abs_Up(Inl ())"
   48.14   (fn prems =>
   48.15          [
   48.16 -        (simp_tac (!simpset addsimps [less_up1b]) 1)
   48.17 +        (simp_tac (simpset() addsimps [less_up1b]) 1)
   48.18          ]);
   48.19  
   48.20  qed_goal "less_up2c" thy "(Iup(x)<<Iup(y)) = (x<<y)"
   48.21   (fn prems =>
   48.22          [
   48.23 -        (simp_tac (!simpset addsimps [less_up1c]) 1)
   48.24 +        (simp_tac (simpset() addsimps [less_up1c]) 1)
   48.25          ]);
   48.26  
   48.27  (* ------------------------------------------------------------------------ *)
    49.1 --- a/src/HOLCF/Up3.ML	Mon Nov 03 12:36:48 1997 +0100
    49.2 +++ b/src/HOLCF/Up3.ML	Mon Nov 03 14:06:27 1997 +0100
    49.3 @@ -188,7 +188,7 @@
    49.4          (asm_simp_tac (Up0_ss addsimps [cont_Iup]) 1)
    49.5          ]);
    49.6  
    49.7 -val tac = (simp_tac (!simpset addsimps [cont_Iup,cont_Ifup1,
    49.8 +val tac = (simp_tac (simpset() addsimps [cont_Iup,cont_Ifup1,
    49.9                  cont_Ifup2,cont2cont_CF1L]) 1);
   49.10  
   49.11  qed_goalw "fup1" thy [up_def,fup_def] "fup`f`UU=UU"
   49.12 @@ -337,8 +337,8 @@
   49.13   (fn prems =>
   49.14          [
   49.15          (res_inst_tac [("p","x")] upE1 1),
   49.16 -        (asm_simp_tac ((simpset_of "Cfun3") addsimps [fup1,fup2]) 1),
   49.17 -        (asm_simp_tac ((simpset_of "Cfun3") addsimps [fup1,fup2]) 1)
   49.18 +        (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1),
   49.19 +        (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1)
   49.20          ]);
   49.21  
   49.22  (* ------------------------------------------------------------------------ *)
    50.1 --- a/src/HOLCF/domain/theorems.ML	Mon Nov 03 12:36:48 1997 +0100
    50.2 +++ b/src/HOLCF/domain/theorems.ML	Mon Nov 03 14:06:27 1997 +0100
    50.3 @@ -373,7 +373,7 @@
    50.4  (* ----- theorems concerning finite approximation and finite induction ------ *)
    50.5  
    50.6  local
    50.7 -  val iterate_Cprod_ss = simpset_of "Fix"
    50.8 +  val iterate_Cprod_ss = simpset_of Fix.thy
    50.9                           addsimps [cfst_strict, csnd_strict]addsimps Cprod_rews;
   50.10    val copy_con_rews  = copy_rews @ con_rews;
   50.11    val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
    51.1 --- a/src/HOLCF/ex/Dagstuhl.ML	Mon Nov 03 12:36:48 1997 +0100
    51.2 +++ b/src/HOLCF/ex/Dagstuhl.ML	Mon Nov 03 14:06:27 1997 +0100
    51.3 @@ -34,10 +34,10 @@
    51.4  val prems = goal Dagstuhl.thy "YS = YYS";
    51.5  by (resolve_tac stream.take_lemmas 1);
    51.6  by (nat_ind_tac "n" 1);
    51.7 -by (simp_tac (!simpset addsimps stream.rews) 1);
    51.8 +by (simp_tac (simpset() addsimps stream.rews) 1);
    51.9  by (stac YS_def2 1);
   51.10  by (stac YYS_def2 1);
   51.11 -by (asm_simp_tac (!simpset addsimps stream.rews) 1);
   51.12 +by (asm_simp_tac (simpset() addsimps stream.rews) 1);
   51.13  by (rtac (lemma5 RS sym RS subst) 1);
   51.14  by (rtac refl 1);
   51.15  val wir_moel=result();
   51.16 @@ -53,7 +53,7 @@
   51.17  by (rtac fix_least 1);
   51.18  by (stac beta_cfun 1);
   51.19  by (cont_tacR 1);
   51.20 -by (simp_tac (!simpset addsimps [YS_def2 RS sym]) 1);
   51.21 +by (simp_tac (simpset() addsimps [YS_def2 RS sym]) 1);
   51.22  val lemma6=result();
   51.23  
   51.24  val prems = goal Dagstuhl.thy "YS << YYS";
    52.1 --- a/src/HOLCF/ex/Dnat.ML	Mon Nov 03 12:36:48 1997 +0100
    52.2 +++ b/src/HOLCF/ex/Dnat.ML	Mon Nov 03 14:06:27 1997 +0100
    52.3 @@ -56,12 +56,12 @@
    52.4  	(res_inst_tac [("x","y")] dnat.casedist 1),
    52.5  	(fast_tac (HOL_cs addSIs [UU_I]) 1),
    52.6  	(Asm_simp_tac 1),
    52.7 -	(asm_simp_tac (!simpset addsimps dnat.dist_les) 1),
    52.8 +	(asm_simp_tac (simpset() addsimps dnat.dist_les) 1),
    52.9  	(rtac allI 1),
   52.10  	(res_inst_tac [("x","y")] dnat.casedist 1),
   52.11  	(fast_tac (HOL_cs addSIs [UU_I]) 1),
   52.12 -	(asm_simp_tac (!simpset addsimps dnat.dist_les) 1),
   52.13 -	(asm_simp_tac (!simpset addsimps dnat.rews) 1),
   52.14 +	(asm_simp_tac (simpset() addsimps dnat.dist_les) 1),
   52.15 +	(asm_simp_tac (simpset() addsimps dnat.rews) 1),
   52.16  	(strip_tac 1),
   52.17  	(subgoal_tac "d<<da" 1),
   52.18  	(etac allE 1),
    53.1 --- a/src/HOLCF/ex/Hoare.ML	Mon Nov 03 12:36:48 1997 +0100
    53.2 +++ b/src/HOLCF/ex/Hoare.ML	Mon Nov 03 14:06:27 1997 +0100
    53.3 @@ -136,7 +136,7 @@
    53.4          (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1),
    53.5          (rtac mp 1),
    53.6          (etac spec 1),
    53.7 -        (simp_tac (!simpset addsimps [less_Suc_eq]) 1),
    53.8 +        (simp_tac (simpset() addsimps [less_Suc_eq]) 1),
    53.9          (simp_tac HOLCF_ss 1),
   53.10          (etac mp 1),
   53.11          (strip_tac 1),
   53.12 @@ -153,7 +153,7 @@
   53.13          [
   53.14          (nat_ind_tac "k" 1),
   53.15          (Simp_tac 1),
   53.16 -(simp_tac (!simpset addsimps [less_Suc_eq]) 1),
   53.17 +(simp_tac (simpset() addsimps [less_Suc_eq]) 1),
   53.18          (strip_tac 1),
   53.19          (res_inst_tac [("s","q`(iterate k g x)")] trans 1),
   53.20          (rtac trans 1),
   53.21 @@ -210,7 +210,7 @@
   53.22          (simp_tac HOLCF_ss 1),
   53.23          (rtac trans 1),
   53.24          (rtac p_def3 1),
   53.25 -        (simp_tac (!simpset delsimps [iterate_Suc]
   53.26 +        (simp_tac (simpset() delsimps [iterate_Suc]
   53.27                              addsimps [iterate_Suc RS sym]) 1),
   53.28          (eres_inst_tac [("s","FF")] ssubst 1),
   53.29          (simp_tac HOLCF_ss 1)
    54.1 --- a/src/HOLCF/ex/Loop.ML	Mon Nov 03 12:36:48 1997 +0100
    54.2 +++ b/src/HOLCF/ex/Loop.ML	Mon Nov 03 14:06:27 1997 +0100
    54.3 @@ -119,7 +119,7 @@
    54.4          (nat_ind_tac "k" 1),
    54.5          (Asm_simp_tac 1),
    54.6          (strip_tac 1),
    54.7 -        (simp_tac (!simpset addsimps [step_def2]) 1),
    54.8 +        (simp_tac (simpset() addsimps [step_def2]) 1),
    54.9          (res_inst_tac [("p","b`(iterate k (step`b`g) x)")] trE 1),
   54.10          (etac notE 1),
   54.11          (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1),
    55.1 --- a/src/HOLCF/ex/Stream.ML	Mon Nov 03 12:36:48 1997 +0100
    55.2 +++ b/src/HOLCF/ex/Stream.ML	Mon Nov 03 14:06:27 1997 +0100
    55.3 @@ -169,14 +169,14 @@
    55.4  val stream_take_lemma2 = prove_goal thy 
    55.5   "! s2. stream_take n`s2 = s2 --> stream_take (Suc n)`s2=s2" (fn prems => [
    55.6  	(nat_ind_tac "n" 1),
    55.7 -	(simp_tac (!simpset addsimps stream_rews) 1),
    55.8 +	(simp_tac (simpset() addsimps stream_rews) 1),
    55.9  	(strip_tac 1),
   55.10  	(hyp_subst_tac  1),
   55.11 -	(simp_tac (!simpset addsimps stream_rews) 1),
   55.12 +	(simp_tac (simpset() addsimps stream_rews) 1),
   55.13  	(rtac allI 1),
   55.14  	(res_inst_tac [("s","s2")] streamE 1),
   55.15 -	(asm_simp_tac (!simpset addsimps stream_rews) 1),
   55.16 -	(asm_simp_tac (!simpset addsimps stream_rews) 1),
   55.17 +	(asm_simp_tac (simpset() addsimps stream_rews) 1),
   55.18 +	(asm_simp_tac (simpset() addsimps stream_rews) 1),
   55.19  	(strip_tac 1 ),
   55.20  	(subgoal_tac "stream_take n1`xs = xs" 1),
   55.21  	(rtac ((hd stream_inject) RS conjunct2) 2),