added local simpsets
authorclasohm
Wed Oct 04 14:01:44 1995 +0100 (1995-10-04)
changeset 1267bca91b4e1710
parent 1266 3ae9fe3c0f68
child 1268 f6ef556b3ede
added local simpsets
src/HOLCF/Cfun3.ML
src/HOLCF/Cont.ML
src/HOLCF/Cprod1.ML
src/HOLCF/Cprod2.ML
src/HOLCF/Cprod3.ML
src/HOLCF/Dlist.ML
src/HOLCF/Dnat.ML
src/HOLCF/Dnat2.ML
src/HOLCF/Fix.ML
src/HOLCF/HOLCF.ML
src/HOLCF/Lift1.ML
src/HOLCF/Lift2.ML
src/HOLCF/Lift3.ML
src/HOLCF/One.ML
src/HOLCF/Pcpo.ML
src/HOLCF/Porder.ML
src/HOLCF/ROOT.ML
src/HOLCF/Sprod0.ML
src/HOLCF/Sprod1.ML
src/HOLCF/Sprod3.ML
src/HOLCF/Ssum0.ML
src/HOLCF/Ssum1.ML
src/HOLCF/Ssum2.ML
src/HOLCF/Ssum3.ML
src/HOLCF/Stream.ML
src/HOLCF/Stream2.ML
src/HOLCF/Tr1.ML
src/HOLCF/Tr2.ML
src/HOLCF/ccc1.ML
src/HOLCF/ex/Coind.ML
src/HOLCF/ex/Dagstuhl.ML
src/HOLCF/ex/Hoare.ML
src/HOLCF/ex/Loop.ML
     1.1 --- a/src/HOLCF/Cfun3.ML	Wed Oct 04 13:12:14 1995 +0100
     1.2 +++ b/src/HOLCF/Cfun3.ML	Wed Oct 04 14:01:44 1995 +0100
     1.3 @@ -224,7 +224,7 @@
     1.4  	"Istrictify(f)(UU)= (UU)"
     1.5   (fn prems =>
     1.6  	[
     1.7 -	(simp_tac HOL_ss 1)
     1.8 +	(Simp_tac 1)
     1.9  	]);
    1.10  
    1.11  qed_goalw "Istrictify2" Cfun3.thy [Istrictify_def]
    1.12 @@ -232,7 +232,7 @@
    1.13   (fn prems =>
    1.14  	[
    1.15  	(cut_facts_tac prems 1),
    1.16 -	(asm_simp_tac HOL_ss 1)
    1.17 +	(Asm_simp_tac 1)
    1.18  	]);
    1.19  
    1.20  qed_goal "monofun_Istrictify1" Cfun3.thy "monofun(Istrictify)"
    1.21 @@ -384,16 +384,14 @@
    1.22  (* Instantiate the simplifier                                               *)
    1.23  (* ------------------------------------------------------------------------ *)
    1.24  
    1.25 -val Cfun_rews  = [minimal,refl_less,beta_cfun,strict_fapp1,strictify1,
    1.26 -		strictify2];
    1.27 +Addsimps [minimal,refl_less,beta_cfun,strict_fapp1,strictify1, strictify2];
    1.28 +
    1.29  
    1.30  (* ------------------------------------------------------------------------ *)
    1.31  (* use cont_tac as autotac.                                                *)
    1.32  (* ------------------------------------------------------------------------ *)
    1.33  
    1.34 -val Cfun_ss = HOL_ss 
    1.35 -	addsimps  Cfun_rews 
    1.36 -	setsolver 
    1.37 -	(fn thms => (resolve_tac (TrueI::refl::thms)) ORELSE' atac ORELSE'
    1.38 -		    (fn i => DEPTH_SOLVE_1 (cont_tac i))
    1.39 -	);
    1.40 +simpset := !simpset setsolver 
    1.41 +           (fn thms => (resolve_tac (TrueI::refl::thms)) ORELSE' atac ORELSE'
    1.42 +                       (fn i => DEPTH_SOLVE_1 (cont_tac i))
    1.43 +           );
     2.1 --- a/src/HOLCF/Cont.ML	Wed Oct 04 13:12:14 1995 +0100
     2.2 +++ b/src/HOLCF/Cont.ML	Wed Oct 04 14:01:44 1995 +0100
     2.3 @@ -147,7 +147,7 @@
     2.4  	(rtac (binchain_cont RS is_ub_lub) 2),
     2.5  	(atac 2),
     2.6  	(atac 2),
     2.7 -	(simp_tac nat_ss 1)
     2.8 +	(Simp_tac 1)
     2.9  	]);
    2.10  
    2.11  (* ------------------------------------------------------------------------ *)
     3.1 --- a/src/HOLCF/Cprod1.ML	Wed Oct 04 13:12:14 1995 +0100
     3.2 +++ b/src/HOLCF/Cprod1.ML	Wed Oct 04 14:01:44 1995 +0100
     3.3 @@ -40,7 +40,7 @@
     3.4  	(res_inst_tac [("p","p")] PairE 1),
     3.5  	(hyp_subst_tac 1),
     3.6  	(dtac less_cprod2a 1),
     3.7 -	(asm_simp_tac HOL_ss 1)
     3.8 +	(Asm_simp_tac 1)
     3.9  	]);
    3.10  
    3.11  qed_goalw "less_cprod2c" Cprod1.thy [less_cprod_def]
    3.12 @@ -65,13 +65,7 @@
    3.13  (* ------------------------------------------------------------------------ *)
    3.14  
    3.15  qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "less_cprod p p"
    3.16 - (fn prems =>
    3.17 -	[
    3.18 -	(res_inst_tac [("p","p")] PairE 1),
    3.19 -	(hyp_subst_tac 1),
    3.20 -	(simp_tac prod_ss 1),
    3.21 -	(simp_tac Cfun_ss 1)
    3.22 -	]);
    3.23 + (fn prems => [Simp_tac 1]);
    3.24  
    3.25  qed_goal "antisym_less_cprod" Cprod1.thy 
    3.26   "[|less_cprod p1 p2;less_cprod p2 p1|] ==> p1=p2"
    3.27 @@ -105,7 +99,7 @@
    3.28  	(dtac less_cprod2c 1),
    3.29  	(dtac less_cprod2c 1),
    3.30  	(rtac (less_cprod1b RS ssubst) 1),
    3.31 -	(simp_tac prod_ss 1),
    3.32 +	(Simp_tac 1),
    3.33  	(etac conjE 1),
    3.34  	(etac conjE 1),
    3.35  	(rtac conjI 1),
     4.1 --- a/src/HOLCF/Cprod2.ML	Wed Oct 04 13:12:14 1995 +0100
     4.2 +++ b/src/HOLCF/Cprod2.ML	Wed Oct 04 14:01:44 1995 +0100
     4.3 @@ -16,10 +16,7 @@
     4.4  	(rtac (inst_cprod_po RS ssubst) 1),
     4.5  	(rtac (less_cprod1b RS ssubst) 1),
     4.6  	(hyp_subst_tac 1),
     4.7 -	(asm_simp_tac prod_ss  1),
     4.8 -	(rtac conjI 1),
     4.9 -	(rtac minimal 1),
    4.10 -	(rtac minimal 1)
    4.11 +	(Asm_simp_tac  1)
    4.12  	]);
    4.13  
    4.14  qed_goal "less_cprod3b" Cprod2.thy
    4.15 @@ -80,8 +77,7 @@
    4.16  	(rtac (less_fun RS iffD2) 1),
    4.17  	(strip_tac 1),
    4.18  	(rtac (less_cprod3b RS iffD2) 1),
    4.19 -	(simp_tac prod_ss 1),
    4.20 -	(asm_simp_tac Cfun_ss 1)
    4.21 +	(Simp_tac 1)
    4.22  	]);
    4.23  
    4.24  qed_goalw "monofun_pair2" Cprod2.thy [monofun] "monofun(Pair(x))"
    4.25 @@ -89,8 +85,7 @@
    4.26  	[
    4.27  	(strip_tac 1),
    4.28  	(rtac (less_cprod3b RS iffD2) 1),
    4.29 -	(simp_tac prod_ss 1),
    4.30 -	(asm_simp_tac Cfun_ss 1)
    4.31 +	(Simp_tac 1)
    4.32  	]);
    4.33  
    4.34  qed_goal "monofun_pair" Cprod2.thy 
    4.35 @@ -118,7 +113,7 @@
    4.36  	(hyp_subst_tac 1),
    4.37  	(res_inst_tac [("p","y")] PairE 1),
    4.38  	(hyp_subst_tac 1),
    4.39 -	(asm_simp_tac prod_ss  1),
    4.40 +	(Asm_simp_tac  1),
    4.41  	(etac (less_cprod4c RS conjunct1) 1)
    4.42  	]);
    4.43  
    4.44 @@ -130,7 +125,7 @@
    4.45  	(hyp_subst_tac 1),
    4.46  	(res_inst_tac [("p","y")] PairE 1),
    4.47  	(hyp_subst_tac 1),
    4.48 -	(asm_simp_tac prod_ss  1),
    4.49 +	(Asm_simp_tac  1),
    4.50  	(etac (less_cprod4c RS conjunct2) 1)
    4.51  	]);
    4.52  
     5.1 --- a/src/HOLCF/Cprod3.ML	Wed Oct 04 13:12:14 1995 +0100
     5.2 +++ b/src/HOLCF/Cprod3.ML	Wed Oct 04 14:01:44 1995 +0100
     5.3 @@ -27,9 +27,9 @@
     5.4  	(rtac (monofun_pair1 RS ch2ch_monofun) 1),
     5.5  	(atac 1),
     5.6  	(rtac allI 1),
     5.7 -	(simp_tac prod_ss 1),
     5.8 +	(Simp_tac 1),
     5.9  	(rtac sym 1),
    5.10 -	(simp_tac prod_ss 1),
    5.11 +	(Simp_tac 1),
    5.12  	(rtac (lub_const RS thelubI) 1)
    5.13  	]);
    5.14  
    5.15 @@ -58,7 +58,7 @@
    5.16  	(cut_facts_tac prems 1),
    5.17  	(res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1),
    5.18  	(rtac sym 1),
    5.19 -	(simp_tac prod_ss 1),
    5.20 +	(Simp_tac 1),
    5.21  	(rtac (lub_const RS thelubI) 1),
    5.22  	(rtac lub_equal 1),
    5.23  	(atac 1),
    5.24 @@ -66,7 +66,7 @@
    5.25  	(rtac (monofun_pair2 RS ch2ch_monofun) 1),
    5.26  	(atac 1),
    5.27  	(rtac allI 1),
    5.28 -	(simp_tac prod_ss 1)
    5.29 +	(Simp_tac 1)
    5.30  	]);
    5.31  
    5.32  qed_goal "contlub_pair2" Cprod3.thy "contlub(Pair(x))"
    5.33 @@ -103,7 +103,7 @@
    5.34  	(strip_tac 1),
    5.35  	(rtac (lub_cprod RS thelubI RS ssubst) 1),
    5.36  	(atac 1),
    5.37 -	(simp_tac prod_ss 1)
    5.38 +	(Simp_tac 1)
    5.39  	]);
    5.40  
    5.41  qed_goal "contlub_snd" Cprod3.thy "contlub(snd)"
    5.42 @@ -113,7 +113,7 @@
    5.43  	(strip_tac 1),
    5.44  	(rtac (lub_cprod RS thelubI RS ssubst) 1),
    5.45  	(atac 1),
    5.46 -	(simp_tac prod_ss 1)
    5.47 +	(Simp_tac 1)
    5.48  	]);
    5.49  
    5.50  qed_goal "cont_fst" Cprod3.thy "cont(fst)"
    5.51 @@ -214,7 +214,7 @@
    5.52  	(rtac (beta_cfun_cprod RS ssubst) 1),
    5.53  	(rtac (beta_cfun RS ssubst) 1),
    5.54  	(rtac cont_fst 1),
    5.55 -	(simp_tac prod_ss  1)
    5.56 +	(Simp_tac  1)
    5.57  	]);
    5.58  
    5.59  qed_goalw "csnd2" Cprod3.thy [csnd_def,cpair_def] 
    5.60 @@ -225,7 +225,7 @@
    5.61  	(rtac (beta_cfun_cprod RS ssubst) 1),
    5.62  	(rtac (beta_cfun RS ssubst) 1),
    5.63  	(rtac cont_snd 1),
    5.64 -	(simp_tac prod_ss  1)
    5.65 +	(Simp_tac  1)
    5.66  	]);
    5.67  
    5.68  qed_goalw "surjective_pairing_Cprod2" Cprod3.thy 
    5.69 @@ -295,8 +295,8 @@
    5.70  	[
    5.71  	(rtac (beta_cfun RS ssubst) 1),
    5.72  	(cont_tacR 1),
    5.73 -	(simp_tac Cfun_ss 1),
    5.74 -	(simp_tac (Cfun_ss addsimps [cfst2,csnd2]) 1)
    5.75 +	(Simp_tac 1),
    5.76 +	(simp_tac (!simpset addsimps [cfst2,csnd2]) 1)
    5.77  	]);
    5.78  
    5.79  qed_goalw "csplit3" Cprod3.thy [csplit_def]
    5.80 @@ -305,14 +305,12 @@
    5.81  	[
    5.82  	(rtac (beta_cfun RS ssubst) 1),
    5.83  	(cont_tacR 1),
    5.84 -	(simp_tac (Cfun_ss addsimps [surjective_pairing_Cprod2]) 1)
    5.85 +	(simp_tac (!simpset addsimps [surjective_pairing_Cprod2]) 1)
    5.86  	]);
    5.87  
    5.88  (* ------------------------------------------------------------------------ *)
    5.89  (* install simplifier for Cprod                                             *)
    5.90  (* ------------------------------------------------------------------------ *)
    5.91  
    5.92 -val Cprod_rews = [cfst2,csnd2,csplit2];
    5.93 +Addsimps [cfst2,csnd2,csplit2];
    5.94  
    5.95 -val Cprod_ss = Cfun_ss addsimps Cprod_rews;
    5.96 -
     6.1 --- a/src/HOLCF/Dlist.ML	Wed Oct 04 13:12:14 1995 +0100
     6.2 +++ b/src/HOLCF/Dlist.ML	Wed Oct 04 14:01:44 1995 +0100
     6.3 @@ -25,7 +25,7 @@
     6.4  val temp = prove_goalw Dlist.thy  [dlist_copy_def] "dlist_copy`f`UU=UU"
     6.5   (fn prems =>
     6.6  	[
     6.7 -	(asm_simp_tac (HOLCF_ss addsimps 
     6.8 +	(asm_simp_tac (!simpset addsimps 
     6.9  		(dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
    6.10  	]);
    6.11  
    6.12 @@ -36,7 +36,7 @@
    6.13      "dlist_copy`f`dnil=dnil"
    6.14   (fn prems =>
    6.15  	[
    6.16 -	(asm_simp_tac (HOLCF_ss addsimps 
    6.17 +	(asm_simp_tac (!simpset addsimps 
    6.18  		(dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
    6.19  	]);
    6.20  
    6.21 @@ -48,11 +48,11 @@
    6.22   (fn prems =>
    6.23  	[
    6.24  	(cut_facts_tac prems 1),
    6.25 -	(asm_simp_tac (HOLCF_ss addsimps 
    6.26 +	(asm_simp_tac (!simpset addsimps 
    6.27  		(dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1),
    6.28  	(res_inst_tac [("Q","x=UU")] classical2 1),
    6.29 -	(asm_simp_tac HOLCF_ss  1),
    6.30 -	(asm_simp_tac (HOLCF_ss addsimps [defined_spair]) 1)
    6.31 +	(Asm_simp_tac  1),
    6.32 +	(asm_simp_tac (!simpset addsimps [defined_spair]) 1)
    6.33  	]);
    6.34  
    6.35  val dlist_copy = temp :: dlist_copy;
    6.36 @@ -67,23 +67,23 @@
    6.37  	"l = UU | l = dnil | (? x xl. x~=UU &xl~=UU & l = dcons`x`xl)"
    6.38   (fn prems =>
    6.39  	[
    6.40 -	(simp_tac HOLCF_ss  1),
    6.41 +	(Simp_tac 1),
    6.42  	(rtac (dlist_rep_iso RS subst) 1),
    6.43  	(res_inst_tac [("p","dlist_rep`l")] ssumE 1),
    6.44  	(rtac disjI1 1),
    6.45 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
    6.46 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
    6.47  	(rtac disjI2 1),
    6.48  	(rtac disjI1 1),
    6.49  	(res_inst_tac [("p","x")] oneE 1),
    6.50  	(contr_tac 1),
    6.51 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
    6.52 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
    6.53  	(rtac disjI2 1),
    6.54  	(rtac disjI2 1),
    6.55  	(res_inst_tac [("p","y")] sprodE 1),
    6.56  	(contr_tac 1),
    6.57  	(rtac exI 1),
    6.58  	(rtac exI 1),
    6.59 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
    6.60 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
    6.61  	(fast_tac HOL_cs 1)
    6.62  	]);
    6.63  
    6.64 @@ -111,7 +111,7 @@
    6.65  val temp = prove_goalw  Dlist.thy  [dlist_when_def] "dlist_when`f1`f2`UU=UU"
    6.66   (fn prems =>
    6.67  	[
    6.68 -	(asm_simp_tac (HOLCF_ss addsimps [dlist_iso_strict]) 1)
    6.69 +	(asm_simp_tac (!simpset addsimps [dlist_iso_strict]) 1)
    6.70  	]);
    6.71  
    6.72  val dlist_when = [temp];
    6.73 @@ -120,7 +120,7 @@
    6.74   "dlist_when`f1`f2`dnil= f1"
    6.75   (fn prems =>
    6.76  	[
    6.77 -	(asm_simp_tac (HOLCF_ss addsimps [dlist_abs_iso]) 1)
    6.78 +	(asm_simp_tac (!simpset addsimps [dlist_abs_iso]) 1)
    6.79  	]);
    6.80  
    6.81  val dlist_when = temp::dlist_when;
    6.82 @@ -130,7 +130,7 @@
    6.83   (fn prems =>
    6.84  	[
    6.85  	(cut_facts_tac prems 1),
    6.86 -	(asm_simp_tac (HOLCF_ss addsimps [dlist_abs_iso,defined_spair]) 1)
    6.87 +	(asm_simp_tac (!simpset addsimps [dlist_abs_iso,defined_spair]) 1)
    6.88  	]);
    6.89  
    6.90  val dlist_when = temp::dlist_when;
    6.91 @@ -144,7 +144,7 @@
    6.92  fun prover defs thm = prove_goalw Dlist.thy defs thm
    6.93   (fn prems =>
    6.94  	[
    6.95 -	(simp_tac (HOLCF_ss addsimps dlist_rews) 1)
    6.96 +	(simp_tac (!simpset addsimps dlist_rews) 1)
    6.97  	]);
    6.98  
    6.99  val dlist_discsel = [
   6.100 @@ -158,7 +158,7 @@
   6.101   (fn prems =>
   6.102  	[
   6.103  	(cut_facts_tac prems 1),
   6.104 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   6.105 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1)
   6.106  	]);
   6.107  
   6.108  val dlist_discsel = [
   6.109 @@ -189,10 +189,10 @@
   6.110   (fn prems =>
   6.111  	[
   6.112  	(res_inst_tac [("P1",contr)] classical3 1),
   6.113 -	(simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.114 +	(simp_tac (!simpset addsimps dlist_rews) 1),
   6.115  	(dtac sym 1),
   6.116 -	(asm_simp_tac HOLCF_ss  1),
   6.117 -	(simp_tac (HOLCF_ss addsimps (prems @ dlist_rews)) 1)
   6.118 +	(Asm_simp_tac  1),
   6.119 +	(simp_tac (!simpset addsimps (prems @ dlist_rews)) 1)
   6.120  	]);
   6.121  
   6.122  
   6.123 @@ -206,7 +206,7 @@
   6.124  fun prover defs thm = prove_goalw Dlist.thy defs thm
   6.125   (fn prems =>
   6.126  	[
   6.127 -	(simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   6.128 +	(simp_tac (!simpset addsimps dlist_rews) 1)
   6.129  	]);
   6.130  
   6.131  val dlist_constrdef = [
   6.132 @@ -228,12 +228,12 @@
   6.133  	(resolve_tac dist_less_tr 1),
   6.134  	(dres_inst_tac [("fo5","is_dnil")] monofun_cfun_arg 1),
   6.135  	(etac box_less 1),
   6.136 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.137 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.138  	(res_inst_tac [("Q","(x::'a)=UU")] classical2 1),
   6.139 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.140 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.141  	(res_inst_tac [("Q","(xl ::'a dlist)=UU")] classical2 1),
   6.142 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.143 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   6.144 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.145 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1)
   6.146  	]);
   6.147  
   6.148  val dlist_dist_less = [temp];
   6.149 @@ -246,8 +246,8 @@
   6.150  	(resolve_tac dist_less_tr 1),
   6.151  	(dres_inst_tac [("fo5","is_dcons")] monofun_cfun_arg 1),
   6.152  	(etac box_less 1),
   6.153 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.154 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   6.155 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.156 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1)
   6.157  	]);
   6.158  
   6.159  val dlist_dist_less = temp::dlist_dist_less;
   6.160 @@ -256,15 +256,15 @@
   6.161   (fn prems =>
   6.162  	[
   6.163  	(res_inst_tac [("Q","x=UU")] classical2 1),
   6.164 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.165 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.166  	(res_inst_tac [("Q","xl=UU")] classical2 1),
   6.167 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.168 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.169  	(res_inst_tac [("P1","TT = FF")] classical3 1),
   6.170  	(resolve_tac dist_eq_tr 1),
   6.171  	(dres_inst_tac [("f","is_dnil")] cfun_arg_cong 1),
   6.172  	(etac box_equals 1),
   6.173 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.174 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   6.175 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.176 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1)
   6.177  	]);
   6.178  
   6.179  val dlist_dist_eq = [temp,temp RS not_sym];
   6.180 @@ -283,12 +283,12 @@
   6.181  	(rtac conjI 1),
   6.182  	(dres_inst_tac [("fo5","dlist_when`UU`(LAM x l.x)")] monofun_cfun_arg 1),
   6.183  	(etac box_less 1),
   6.184 -	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
   6.185 -	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
   6.186 +	(asm_simp_tac (!simpset addsimps dlist_when) 1),
   6.187 +	(asm_simp_tac (!simpset addsimps dlist_when) 1),
   6.188  	(dres_inst_tac [("fo5","dlist_when`UU`(LAM x l.l)")] monofun_cfun_arg 1),
   6.189  	(etac box_less 1),
   6.190 -	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
   6.191 -	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1)
   6.192 +	(asm_simp_tac (!simpset addsimps dlist_when) 1),
   6.193 +	(asm_simp_tac (!simpset addsimps dlist_when) 1)
   6.194  	]);
   6.195  
   6.196  val dlist_invert =[temp];
   6.197 @@ -305,12 +305,12 @@
   6.198  	(rtac conjI 1),
   6.199  	(dres_inst_tac [("f","dlist_when`UU`(LAM x l.x)")] cfun_arg_cong 1),
   6.200  	(etac box_equals 1),
   6.201 -	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
   6.202 -	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
   6.203 +	(asm_simp_tac (!simpset addsimps dlist_when) 1),
   6.204 +	(asm_simp_tac (!simpset addsimps dlist_when) 1),
   6.205  	(dres_inst_tac [("f","dlist_when`UU`(LAM x l.l)")] cfun_arg_cong 1),
   6.206  	(etac box_equals 1),
   6.207 -	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
   6.208 -	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1)
   6.209 +	(asm_simp_tac (!simpset addsimps dlist_when) 1),
   6.210 +	(asm_simp_tac (!simpset addsimps dlist_when) 1)
   6.211  	]);
   6.212  
   6.213  val dlist_inject = [temp];
   6.214 @@ -326,7 +326,7 @@
   6.215  	(cut_facts_tac prems 1),
   6.216  	(rtac dlistE 1),
   6.217  	(contr_tac 1),
   6.218 -	(REPEAT (asm_simp_tac (HOLCF_ss addsimps dlist_discsel) 1))
   6.219 +	(REPEAT (asm_simp_tac (!simpset addsimps dlist_discsel) 1))
   6.220  	]);
   6.221  
   6.222  val dlist_discsel_def = 
   6.223 @@ -346,8 +346,8 @@
   6.224  	[
   6.225  	(cut_facts_tac prems 1),
   6.226  	(res_inst_tac [("Q","x=UU")] classical2 1),
   6.227 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.228 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   6.229 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.230 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1)
   6.231  	]);
   6.232  
   6.233  qed_goal "dtl2" Dlist.thy "x~=UU ==> dtl`(dcons`x`xl)=xl"
   6.234 @@ -355,8 +355,8 @@
   6.235  	[
   6.236  	(cut_facts_tac prems 1),
   6.237  	(res_inst_tac [("Q","xl=UU")] classical2 1),
   6.238 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.239 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   6.240 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.241 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1)
   6.242  	]);
   6.243  
   6.244  val dlist_rews = dhd2 :: dtl2 :: dlist_rews;
   6.245 @@ -369,9 +369,9 @@
   6.246   (fn prems =>
   6.247  	[
   6.248  	(res_inst_tac [("n","n")] natE 1),
   6.249 -	(asm_simp_tac iterate_ss 1),
   6.250 -	(asm_simp_tac iterate_ss 1),
   6.251 -	(simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   6.252 +	(Asm_simp_tac 1),
   6.253 +	(Asm_simp_tac 1),
   6.254 +	(simp_tac (!simpset addsimps dlist_rews) 1)
   6.255  	]);
   6.256  
   6.257  val dlist_take = [temp];
   6.258 @@ -379,7 +379,7 @@
   6.259  val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take 0`xs=UU"
   6.260   (fn prems =>
   6.261  	[
   6.262 -	(asm_simp_tac iterate_ss 1)
   6.263 +	(Asm_simp_tac 1)
   6.264  	]);
   6.265  
   6.266  val dlist_take = temp::dlist_take;
   6.267 @@ -388,8 +388,8 @@
   6.268  	"dlist_take (Suc n)`dnil=dnil"
   6.269   (fn prems =>
   6.270  	[
   6.271 -	(asm_simp_tac iterate_ss 1),
   6.272 -	(simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   6.273 +	(Asm_simp_tac 1),
   6.274 +	(simp_tac (!simpset addsimps dlist_rews) 1)
   6.275  	]);
   6.276  
   6.277  val dlist_take = temp::dlist_take;
   6.278 @@ -399,19 +399,19 @@
   6.279   (fn prems =>
   6.280  	[
   6.281  	(res_inst_tac [("Q","x=UU")] classical2 1),
   6.282 -	(asm_simp_tac iterate_ss 1),
   6.283 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.284 +	(Asm_simp_tac 1),
   6.285 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.286  	(res_inst_tac [("Q","xl=UU")] classical2 1),
   6.287 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.288 -	(asm_simp_tac iterate_ss 1),
   6.289 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.290 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.291 +	(Asm_simp_tac 1),
   6.292 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.293  	(res_inst_tac [("n","n")] natE 1),
   6.294 -	(asm_simp_tac iterate_ss 1),
   6.295 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.296 -	(asm_simp_tac iterate_ss 1),
   6.297 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.298 -	(asm_simp_tac iterate_ss 1),
   6.299 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   6.300 +	(Asm_simp_tac 1),
   6.301 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.302 +	(Asm_simp_tac 1),
   6.303 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.304 +	(Asm_simp_tac 1),
   6.305 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1)
   6.306  	]);
   6.307  
   6.308  val dlist_take = temp::dlist_take;
   6.309 @@ -453,17 +453,17 @@
   6.310  	[
   6.311  	(cut_facts_tac prems 1),
   6.312  	(nat_ind_tac "n" 1),
   6.313 -	(simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.314 +	(simp_tac (!simpset addsimps dlist_rews) 1),
   6.315  	(strip_tac 1),
   6.316  	((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
   6.317  	(atac 1),
   6.318 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.319 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.320  	(etac disjE 1),
   6.321 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.322 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.323  	(etac exE 1),
   6.324  	(etac exE 1),
   6.325  	(etac exE 1),
   6.326 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.327 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.328  	(REPEAT (etac conjE 1)),
   6.329  	(rtac cfun_arg_cong 1),
   6.330  	(fast_tac HOL_cs 1)
   6.331 @@ -489,17 +489,17 @@
   6.332   (fn prems =>
   6.333  	[
   6.334  	(nat_ind_tac "n" 1),
   6.335 -	(simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.336 +	(simp_tac (!simpset addsimps dlist_rews) 1),
   6.337  	(resolve_tac prems 1),
   6.338  	(rtac allI 1),
   6.339  	(res_inst_tac [("l","l")] dlistE 1),
   6.340 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.341 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.342  	(resolve_tac prems 1),
   6.343 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.344 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.345  	(resolve_tac prems 1),
   6.346 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.347 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.348  	(res_inst_tac [("Q","dlist_take n1`xl=UU")] classical2 1),
   6.349 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.350 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.351  	(resolve_tac prems 1),
   6.352  	(resolve_tac prems 1),
   6.353  	(atac 1),
   6.354 @@ -512,28 +512,28 @@
   6.355   (fn prems =>
   6.356  	[
   6.357  	(nat_ind_tac "n" 1),
   6.358 -	(simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.359 +	(simp_tac (!simpset addsimps dlist_rews) 1),
   6.360  	(rtac allI 1),
   6.361  	(res_inst_tac [("l","l")] dlistE 1),
   6.362 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.363 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.364 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.365 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.366 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.367 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.368  	(eres_inst_tac [("x","xl")] allE 1),
   6.369  	(etac disjE 1),
   6.370 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.371 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   6.372 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.373 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1)
   6.374  	]);
   6.375  
   6.376  qed_goal "dlist_all_finite_lemma2" Dlist.thy "? n.dlist_take n`l=l"
   6.377   (fn prems =>
   6.378  	[
   6.379  	(res_inst_tac [("Q","l=UU")] classical2 1),
   6.380 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.381 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.382  	(subgoal_tac "(!n.dlist_take n`l=UU) |(? n.dlist_take n`l = l)" 1),
   6.383  	(etac disjE 1),
   6.384  	(eres_inst_tac [("P","l=UU")] notE 1),
   6.385  	(rtac dlist_take_lemma 1),
   6.386 -	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   6.387 +	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
   6.388  	(atac 1),
   6.389  	(subgoal_tac "!n.!l.dlist_take n`l=UU |dlist_take n`l=l" 1),
   6.390  	(fast_tac HOL_cs 1),
     7.1 --- a/src/HOLCF/Dnat.ML	Wed Oct 04 13:12:14 1995 +0100
     7.2 +++ b/src/HOLCF/Dnat.ML	Wed Oct 04 14:01:44 1995 +0100
     7.3 @@ -26,7 +26,7 @@
     7.4   (fn prems =>
     7.5  	[
     7.6  	(cut_facts_tac prems 1),
     7.7 -	(asm_simp_tac (HOLCF_ss addsimps 
     7.8 +	(asm_simp_tac (!simpset addsimps 
     7.9  		(dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1)
    7.10  	]);
    7.11  
    7.12 @@ -48,18 +48,18 @@
    7.13  	"n = UU | n = dzero | (? x . x~=UU & n = dsucc`x)"
    7.14   (fn prems =>
    7.15  	[
    7.16 -	(simp_tac HOLCF_ss  1),
    7.17 +	(Simp_tac  1),
    7.18  	(rtac (dnat_rep_iso RS subst) 1),
    7.19  	(res_inst_tac [("p","dnat_rep`n")] ssumE 1),
    7.20  	(rtac disjI1 1),
    7.21 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
    7.22 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
    7.23  	(rtac (disjI1 RS disjI2) 1),
    7.24 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
    7.25 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
    7.26  	(res_inst_tac [("p","x")] oneE 1),
    7.27  	(contr_tac 1),
    7.28 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
    7.29 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
    7.30  	(rtac (disjI2 RS disjI2) 1),
    7.31 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
    7.32 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
    7.33  	(fast_tac HOL_cs 1)
    7.34  	]);
    7.35  
    7.36 @@ -85,7 +85,7 @@
    7.37   (fn prems =>
    7.38  	[
    7.39  	(cut_facts_tac prems 1),
    7.40 -	(asm_simp_tac (HOLCF_ss addsimps 
    7.41 +	(asm_simp_tac (!simpset addsimps 
    7.42  		(dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1)
    7.43  	]);
    7.44  
    7.45 @@ -106,7 +106,7 @@
    7.46  fun prover defs thm = prove_goalw Dnat.thy defs thm
    7.47   (fn prems =>
    7.48  	[
    7.49 -	(simp_tac (HOLCF_ss addsimps dnat_rews) 1)
    7.50 +	(simp_tac (!simpset addsimps dnat_rews) 1)
    7.51  	]);
    7.52  
    7.53  val dnat_discsel = [
    7.54 @@ -120,7 +120,7 @@
    7.55   (fn prems =>
    7.56  	[
    7.57  	(cut_facts_tac prems 1),
    7.58 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
    7.59 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1)
    7.60  	]);
    7.61  
    7.62  val dnat_discsel = [
    7.63 @@ -142,10 +142,10 @@
    7.64   (fn prems =>
    7.65  	[
    7.66  	(res_inst_tac [("P1",contr)] classical3 1),
    7.67 -	(simp_tac (HOLCF_ss addsimps dnat_rews) 1),
    7.68 +	(simp_tac (!simpset addsimps dnat_rews) 1),
    7.69  	(dtac sym 1),
    7.70 -	(asm_simp_tac HOLCF_ss  1),
    7.71 -	(simp_tac (HOLCF_ss addsimps (prems @ dnat_rews)) 1)
    7.72 +	(Asm_simp_tac  1),
    7.73 +	(simp_tac (!simpset addsimps (prems @ dnat_rews)) 1)
    7.74  	]);
    7.75  
    7.76  val dnat_constrdef = [
    7.77 @@ -157,7 +157,7 @@
    7.78  fun prover defs thm = prove_goalw Dnat.thy defs thm
    7.79   (fn prems =>
    7.80  	[
    7.81 -	(simp_tac (HOLCF_ss addsimps dnat_rews) 1)
    7.82 +	(simp_tac (!simpset addsimps dnat_rews) 1)
    7.83  	]);
    7.84  
    7.85  val dnat_constrdef = [
    7.86 @@ -178,10 +178,10 @@
    7.87  	(resolve_tac dist_less_tr 1),
    7.88  	(dres_inst_tac [("fo5","is_dzero")] monofun_cfun_arg 1),
    7.89  	(etac box_less 1),
    7.90 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
    7.91 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
    7.92  	(res_inst_tac [("Q","n=UU")] classical2 1),
    7.93 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
    7.94 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
    7.95 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
    7.96 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1)
    7.97  	]);
    7.98  
    7.99  val dnat_dist_less = [temp];
   7.100 @@ -194,8 +194,8 @@
   7.101  	(resolve_tac dist_less_tr 1),
   7.102  	(dres_inst_tac [("fo5","is_dsucc")] monofun_cfun_arg 1),
   7.103  	(etac box_less 1),
   7.104 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.105 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   7.106 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.107 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1)
   7.108  	]);
   7.109  
   7.110  val dnat_dist_less = temp::dnat_dist_less;
   7.111 @@ -204,13 +204,13 @@
   7.112   (fn prems =>
   7.113  	[
   7.114  	(res_inst_tac [("Q","n=UU")] classical2 1),
   7.115 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.116 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.117  	(res_inst_tac [("P1","TT = FF")] classical3 1),
   7.118  	(resolve_tac dist_eq_tr 1),
   7.119  	(dres_inst_tac [("f","is_dzero")] cfun_arg_cong 1),
   7.120  	(etac box_equals 1),
   7.121 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.122 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   7.123 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.124 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1)
   7.125  	]);
   7.126  
   7.127  val dnat_dist_eq = [temp, temp RS not_sym];
   7.128 @@ -230,8 +230,8 @@
   7.129  	(cut_facts_tac prems 1),
   7.130  	(dres_inst_tac [("fo5","dnat_when`c`(LAM x.x)")] monofun_cfun_arg 1),
   7.131  	(etac box_less 1),
   7.132 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.133 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   7.134 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.135 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1)
   7.136  	])
   7.137  	];
   7.138  
   7.139 @@ -248,8 +248,8 @@
   7.140  	(cut_facts_tac prems 1),
   7.141  	(dres_inst_tac [("f","dnat_when`c`(LAM x.x)")] cfun_arg_cong 1),
   7.142  	(etac box_equals 1),
   7.143 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.144 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   7.145 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.146 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1)
   7.147  	])
   7.148  	];
   7.149  
   7.150 @@ -264,7 +264,7 @@
   7.151  	(cut_facts_tac prems 1),
   7.152  	(rtac dnatE 1),
   7.153  	(contr_tac 1),
   7.154 -	(REPEAT (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1))
   7.155 +	(REPEAT (asm_simp_tac (!simpset addsimps dnat_rews) 1))
   7.156  	]);
   7.157  
   7.158  val dnat_discsel_def = 
   7.159 @@ -283,9 +283,9 @@
   7.160   (fn prems =>
   7.161  	[
   7.162  	(res_inst_tac [("n","n")] natE 1),
   7.163 -	(asm_simp_tac iterate_ss 1),
   7.164 -	(asm_simp_tac iterate_ss 1),
   7.165 -	(simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   7.166 +	(Asm_simp_tac 1),
   7.167 +	(Asm_simp_tac 1),
   7.168 +	(simp_tac (!simpset addsimps dnat_rews) 1)
   7.169  	]);
   7.170  
   7.171  val dnat_take = [temp];
   7.172 @@ -293,7 +293,7 @@
   7.173  val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take 0`xs = UU"
   7.174   (fn prems =>
   7.175  	[
   7.176 -	(asm_simp_tac iterate_ss 1)
   7.177 +	(Asm_simp_tac 1)
   7.178  	]);
   7.179  
   7.180  val dnat_take = temp::dnat_take;
   7.181 @@ -302,8 +302,8 @@
   7.182  	"dnat_take (Suc n)`dzero=dzero"
   7.183   (fn prems =>
   7.184  	[
   7.185 -	(asm_simp_tac iterate_ss 1),
   7.186 -	(simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   7.187 +	(Asm_simp_tac 1),
   7.188 +	(simp_tac (!simpset addsimps dnat_rews) 1)
   7.189  	]);
   7.190  
   7.191  val dnat_take = temp::dnat_take;
   7.192 @@ -313,16 +313,16 @@
   7.193   (fn prems =>
   7.194  	[
   7.195  	(res_inst_tac [("Q","xs=UU")] classical2 1),
   7.196 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.197 -	(asm_simp_tac iterate_ss 1),
   7.198 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.199 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.200 +	(Asm_simp_tac 1),
   7.201 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.202  	(res_inst_tac [("n","n")] natE 1),
   7.203 -	(asm_simp_tac iterate_ss 1),
   7.204 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.205 -	(asm_simp_tac iterate_ss 1),
   7.206 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.207 -	(asm_simp_tac iterate_ss 1),
   7.208 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   7.209 +	(Asm_simp_tac 1),
   7.210 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.211 +	(Asm_simp_tac 1),
   7.212 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.213 +	(Asm_simp_tac 1),
   7.214 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1)
   7.215  	]);
   7.216  
   7.217  val dnat_take = temp::dnat_take;
   7.218 @@ -365,16 +365,16 @@
   7.219  	[
   7.220  	(cut_facts_tac prems 1),
   7.221  	(nat_ind_tac "n" 1),
   7.222 -	(simp_tac (HOLCF_ss addsimps dnat_take) 1),
   7.223 +	(simp_tac (!simpset addsimps dnat_take) 1),
   7.224  	(strip_tac 1),
   7.225  	((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
   7.226  	(atac 1),
   7.227 -	(asm_simp_tac (HOLCF_ss addsimps dnat_take) 1),
   7.228 +	(asm_simp_tac (!simpset addsimps dnat_take) 1),
   7.229  	(etac disjE 1),
   7.230 -	(asm_simp_tac (HOLCF_ss addsimps dnat_take) 1),
   7.231 +	(asm_simp_tac (!simpset addsimps dnat_take) 1),
   7.232  	(etac exE 1),
   7.233  	(etac exE 1),
   7.234 -	(asm_simp_tac (HOLCF_ss addsimps dnat_take) 1),
   7.235 +	(asm_simp_tac (!simpset addsimps dnat_take) 1),
   7.236  	(REPEAT (etac conjE 1)),
   7.237  	(rtac cfun_arg_cong 1),
   7.238  	(fast_tac HOL_cs 1)
   7.239 @@ -409,17 +409,17 @@
   7.240  	(rtac adm_subst 1),
   7.241  	(cont_tacR 1),
   7.242  	(resolve_tac prems 1),
   7.243 -	(simp_tac HOLCF_ss 1),
   7.244 +	(Simp_tac 1),
   7.245  	(resolve_tac prems 1),
   7.246  	(strip_tac 1),
   7.247  	(res_inst_tac [("n","xa")] dnatE 1),
   7.248 -	(asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
   7.249 +	(asm_simp_tac (!simpset addsimps dnat_copy) 1),
   7.250  	(resolve_tac prems 1),
   7.251 -	(asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
   7.252 +	(asm_simp_tac (!simpset addsimps dnat_copy) 1),
   7.253  	(resolve_tac prems 1),
   7.254 -	(asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
   7.255 +	(asm_simp_tac (!simpset addsimps dnat_copy) 1),
   7.256  	(res_inst_tac [("Q","x`xb=UU")] classical2 1),
   7.257 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.258 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.259  	(resolve_tac prems 1),
   7.260  	(eresolve_tac prems 1),
   7.261  	(etac spec 1)
   7.262 @@ -433,17 +433,17 @@
   7.263   (fn prems =>
   7.264  	[
   7.265  	(nat_ind_tac "n" 1),
   7.266 -	(simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.267 +	(simp_tac (!simpset addsimps dnat_rews) 1),
   7.268  	(resolve_tac prems 1),
   7.269  	(rtac allI 1),
   7.270  	(res_inst_tac [("n","s")] dnatE 1),
   7.271 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.272 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.273  	(resolve_tac prems 1),
   7.274 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.275 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.276  	(resolve_tac prems 1),
   7.277 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.278 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.279  	(res_inst_tac [("Q","dnat_take n1`x=UU")] classical2 1),
   7.280 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.281 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.282  	(resolve_tac prems 1),
   7.283  	(resolve_tac prems 1),
   7.284  	(atac 1),
   7.285 @@ -455,28 +455,28 @@
   7.286   (fn prems =>
   7.287  	[
   7.288  	(nat_ind_tac "n" 1),
   7.289 -	(simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.290 +	(simp_tac (!simpset addsimps dnat_rews) 1),
   7.291  	(rtac allI 1),
   7.292  	(res_inst_tac [("n","s")] dnatE 1),
   7.293 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.294 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.295 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.296 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.297 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.298 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.299  	(eres_inst_tac [("x","x")] allE 1),
   7.300  	(etac disjE 1),
   7.301 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.302 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   7.303 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.304 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1)
   7.305  	]);
   7.306  
   7.307  qed_goal "dnat_all_finite_lemma2" Dnat.thy "? n.dnat_take n`s=s"
   7.308   (fn prems =>
   7.309  	[
   7.310  	(res_inst_tac [("Q","s=UU")] classical2 1),
   7.311 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.312 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.313  	(subgoal_tac "(!n.dnat_take(n)`s=UU) |(? n.dnat_take(n)`s=s)" 1),
   7.314  	(etac disjE 1),
   7.315  	(eres_inst_tac [("P","s=UU")] notE 1),
   7.316  	(rtac dnat_take_lemma 1),
   7.317 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.318 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.319  	(atac 1),
   7.320  	(subgoal_tac "!n.!s.dnat_take(n)`s=UU |dnat_take(n)`s=s" 1),
   7.321  	(fast_tac HOL_cs 1),
   7.322 @@ -508,13 +508,13 @@
   7.323  	(rtac allI 1),
   7.324  	(res_inst_tac [("n","y")] dnatE 1),
   7.325  	(fast_tac (HOL_cs addSIs [UU_I]) 1),
   7.326 -	(asm_simp_tac HOLCF_ss 1),
   7.327 -	(asm_simp_tac (HOLCF_ss addsimps dnat_dist_less) 1),
   7.328 +	(Asm_simp_tac 1),
   7.329 +	(asm_simp_tac (!simpset addsimps dnat_dist_less) 1),
   7.330  	(rtac allI 1),
   7.331  	(res_inst_tac [("n","y")] dnatE 1),
   7.332  	(fast_tac (HOL_cs addSIs [UU_I]) 1),
   7.333 -	(asm_simp_tac (HOLCF_ss addsimps dnat_dist_less) 1),
   7.334 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   7.335 +	(asm_simp_tac (!simpset addsimps dnat_dist_less) 1),
   7.336 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.337  	(strip_tac 1),
   7.338  	(subgoal_tac "s1<<xa" 1),
   7.339  	(etac allE 1),
   7.340 @@ -522,7 +522,7 @@
   7.341  	(atac 1),
   7.342  	(etac disjE 1),
   7.343  	(contr_tac 1),
   7.344 -	(asm_simp_tac HOLCF_ss 1),
   7.345 +	(Asm_simp_tac 1),
   7.346  	(resolve_tac  dnat_invert 1),
   7.347  	(REPEAT (atac 1))
   7.348  	]);
     8.1 --- a/src/HOLCF/Dnat2.ML	Wed Oct 04 13:12:14 1995 +0100
     8.2 +++ b/src/HOLCF/Dnat2.ML	Wed Oct 04 14:01:44 1995 +0100
     8.3 @@ -24,14 +24,14 @@
     8.4   (fn prems =>
     8.5  	[
     8.6  	(rtac (iterator_def2 RS ssubst) 1),
     8.7 -	(simp_tac (HOLCF_ss addsimps dnat_when) 1)
     8.8 +	(simp_tac (!simpset addsimps dnat_when) 1)
     8.9  	]);
    8.10  
    8.11  qed_goal "iterator2" Dnat2.thy "iterator`dzero`f`x = x"
    8.12   (fn prems =>
    8.13  	[
    8.14  	(rtac (iterator_def2 RS ssubst) 1),
    8.15 -	(simp_tac (HOLCF_ss addsimps dnat_when) 1)
    8.16 +	(simp_tac (!simpset addsimps dnat_when) 1)
    8.17  	]);
    8.18  
    8.19  qed_goal "iterator3" Dnat2.thy 
    8.20 @@ -41,7 +41,7 @@
    8.21  	(cut_facts_tac prems 1),
    8.22  	(rtac trans 1),
    8.23  	(rtac (iterator_def2 RS ssubst) 1),
    8.24 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
    8.25 +	(asm_simp_tac (!simpset addsimps dnat_rews) 1),
    8.26  	(rtac refl 1)
    8.27  	]);
    8.28  
     9.1 --- a/src/HOLCF/Fix.ML	Wed Oct 04 13:12:14 1995 +0100
     9.2 +++ b/src/HOLCF/Fix.ML	Wed Oct 04 14:01:44 1995 +0100
     9.3 @@ -24,14 +24,14 @@
     9.4  	(resolve_tac (nat_recs iterate_def) 1)
     9.5  	]);
     9.6  
     9.7 -val iterate_ss = Cfun_ss addsimps [iterate_0,iterate_Suc];
     9.8 +Addsimps [iterate_0, iterate_Suc];
     9.9  
    9.10  qed_goal "iterate_Suc2" Fix.thy "iterate (Suc n) F x = iterate n F (F`x)"
    9.11   (fn prems =>
    9.12  	[
    9.13  	(nat_ind_tac "n" 1),
    9.14 -	(simp_tac iterate_ss 1),
    9.15 -	(asm_simp_tac iterate_ss 1)
    9.16 +	(Simp_tac 1),
    9.17 +	(Asm_simp_tac 1)
    9.18  	]);
    9.19  
    9.20  (* ------------------------------------------------------------------------ *)
    9.21 @@ -45,10 +45,10 @@
    9.22  	[
    9.23  	(cut_facts_tac prems 1),
    9.24  	(strip_tac 1),
    9.25 -	(simp_tac iterate_ss 1),
    9.26 +	(Simp_tac 1),
    9.27  	(nat_ind_tac "i" 1),
    9.28 -	(asm_simp_tac iterate_ss 1),
    9.29 -	(asm_simp_tac iterate_ss 1),
    9.30 +	(Asm_simp_tac 1),
    9.31 +	(Asm_simp_tac 1),
    9.32  	(etac monofun_cfun_arg 1)
    9.33  	]);
    9.34  
    9.35 @@ -101,8 +101,8 @@
    9.36  	(rtac ub_rangeI 1),
    9.37  	(strip_tac 1),
    9.38  	(nat_ind_tac "i" 1),
    9.39 -	(asm_simp_tac iterate_ss 1),
    9.40 -	(asm_simp_tac iterate_ss 1),
    9.41 +	(Asm_simp_tac 1),
    9.42 +	(Asm_simp_tac 1),
    9.43  	(res_inst_tac [("t","x")] subst 1),
    9.44  	(atac 1),
    9.45  	(etac monofun_cfun_arg 1)
    9.46 @@ -118,8 +118,8 @@
    9.47  	[
    9.48  	(strip_tac 1),
    9.49  	(nat_ind_tac "i" 1),
    9.50 -	(asm_simp_tac iterate_ss 1),
    9.51 -	(asm_simp_tac iterate_ss 1),
    9.52 +	(Asm_simp_tac 1),
    9.53 +	(Asm_simp_tac 1),
    9.54  	(rtac (less_fun RS iffD2) 1),
    9.55  	(rtac allI 1),
    9.56  	(rtac monofun_cfun 1),
    9.57 @@ -139,9 +139,9 @@
    9.58  	[
    9.59  	(strip_tac 1),
    9.60  	(nat_ind_tac "i" 1),
    9.61 -	(asm_simp_tac iterate_ss 1),
    9.62 +	(Asm_simp_tac 1),
    9.63  	(rtac (lub_const RS thelubI RS sym) 1),
    9.64 -	(asm_simp_tac iterate_ss 1),
    9.65 +	(Asm_simp_tac 1),
    9.66  	(rtac ext 1),
    9.67  	(rtac (thelub_fun RS ssubst) 1),
    9.68  	(rtac is_chainI 1),
    9.69 @@ -183,8 +183,8 @@
    9.70  	(rtac monofunI 1),
    9.71  	(strip_tac 1),
    9.72  	(nat_ind_tac "n" 1),
    9.73 -	(asm_simp_tac iterate_ss 1),
    9.74 -	(asm_simp_tac iterate_ss 1),
    9.75 +	(Asm_simp_tac 1),
    9.76 +	(Asm_simp_tac 1),
    9.77  	(etac monofun_cfun_arg 1)
    9.78  	]);
    9.79  
    9.80 @@ -194,8 +194,8 @@
    9.81  	(rtac contlubI 1),
    9.82  	(strip_tac 1),
    9.83  	(nat_ind_tac "n" 1),
    9.84 -	(simp_tac iterate_ss 1),
    9.85 -	(simp_tac iterate_ss 1),
    9.86 +	(Simp_tac 1),
    9.87 +	(Simp_tac 1),
    9.88  	(res_inst_tac [("t","iterate n1 F (lub(range(%u. Y u)))"),
    9.89  	("s","lub(range(%i. iterate n1 F (Y i)))")] ssubst 1),
    9.90  	(atac 1),
    9.91 @@ -328,7 +328,7 @@
    9.92  qed_goalw "fix_eq" Fix.thy  [fix_def] "fix`F = F`(fix`F)"
    9.93   (fn prems =>
    9.94  	[
    9.95 -	(asm_simp_tac (Cfun_ss addsimps [cont_Ifix]) 1),
    9.96 +	(asm_simp_tac (!simpset addsimps [cont_Ifix]) 1),
    9.97  	(rtac Ifix_eq 1)
    9.98  	]);
    9.99  
   9.100 @@ -336,7 +336,7 @@
   9.101   (fn prems =>
   9.102  	[
   9.103  	(cut_facts_tac prems 1),
   9.104 -	(asm_simp_tac (Cfun_ss addsimps [cont_Ifix]) 1),
   9.105 +	(asm_simp_tac (!simpset addsimps [cont_Ifix]) 1),
   9.106  	(etac Ifix_least 1)
   9.107  	]);
   9.108  
   9.109 @@ -421,7 +421,7 @@
   9.110   (fn prems =>
   9.111  	[
   9.112  	(fold_goals_tac [Ifix_def]),
   9.113 -	(asm_simp_tac (Cfun_ss addsimps [cont_Ifix]) 1)
   9.114 +	(asm_simp_tac (!simpset addsimps [cont_Ifix]) 1)
   9.115  	]);
   9.116  
   9.117  
   9.118 @@ -567,7 +567,7 @@
   9.119  	(atac 2),
   9.120  	(rtac mp 1),
   9.121  	(etac spec 1),
   9.122 -	(asm_simp_tac nat_ss 1)
   9.123 +	(Asm_simp_tac 1)
   9.124  	]);
   9.125  
   9.126  
   9.127 @@ -836,7 +836,7 @@
   9.128   (fn prems =>
   9.129  	[
   9.130  	(res_inst_tac [("P2","%x.False")] (adm_cong RS iffD1) 1),
   9.131 -	(asm_simp_tac Cfun_ss 1),
   9.132 +	(Asm_simp_tac 1),
   9.133  	(rtac adm_not_free 1)
   9.134  	]);
   9.135  
   9.136 @@ -927,19 +927,17 @@
   9.137  	(atac 1),
   9.138  	(atac 1),
   9.139  	(res_inst_tac [("s","False"),("t","Suc(ia) < Suc(i)")] ssubst 1),
   9.140 -	(asm_simp_tac nat_ss  1),
   9.141 +	(Asm_simp_tac  1),
   9.142  	(rtac iffI 1),
   9.143  	(etac FalseE 2),
   9.144  	(rtac notE 1),
   9.145  	(etac less_not_sym 1),	
   9.146  	(atac 1),
   9.147 -	(asm_simp_tac Cfun_ss  1),
   9.148 +	(Asm_simp_tac 1),
   9.149  	(etac (is_chainE RS spec) 1),
   9.150  	(hyp_subst_tac 1),
   9.151 -	(asm_simp_tac nat_ss 1),
   9.152 -	(rtac refl_less 1),
   9.153 -	(asm_simp_tac nat_ss 1),
   9.154 -	(rtac refl_less 1)
   9.155 +	(Asm_simp_tac 1),
   9.156 +	(Asm_simp_tac 1)
   9.157  	]);
   9.158  
   9.159  qed_goal "adm_disj_lemma4"  Fix.thy
   9.160 @@ -951,18 +949,18 @@
   9.161  	(rtac allI 1),
   9.162  	(res_inst_tac [("m","n"),("n","Suc(i)")] nat_less_cases 1),
   9.163  	(res_inst_tac[("s","Y(Suc(i))"),("t","if n<Suc(i) then Y(Suc(i)) else Y n")] ssubst 1),
   9.164 -	(asm_simp_tac nat_ss 1),
   9.165 +	(Asm_simp_tac 1),
   9.166  	(etac allE 1),
   9.167  	(rtac mp 1),
   9.168  	(atac 1),
   9.169 -	(asm_simp_tac nat_ss 1),
   9.170 +	(Asm_simp_tac 1),
   9.171  	(res_inst_tac[("s","Y(n)"),("t","if n<Suc(i) then Y(Suc(i)) else Y(n)")] ssubst 1),
   9.172 -	(asm_simp_tac nat_ss 1),
   9.173 +	(Asm_simp_tac 1),
   9.174  	(hyp_subst_tac 1),
   9.175  	(dtac spec 1),
   9.176  	(rtac mp 1),
   9.177  	(atac 1),
   9.178 -	(asm_simp_tac nat_ss 1),
   9.179 +	(Asm_simp_tac 1),
   9.180  	(res_inst_tac [("s","Y(n)"),("t","if n < Suc(i) then Y(Suc(i)) else Y(n)")] ssubst 1),
   9.181  	(res_inst_tac [("s","False"),("t","n < Suc(i)")] ssubst 1),
   9.182  	(rtac iffI 1),
   9.183 @@ -970,7 +968,7 @@
   9.184  	(rtac notE 1),
   9.185  	(etac less_not_sym 1),	
   9.186  	(atac 1),
   9.187 -	(asm_simp_tac nat_ss 1),
   9.188 +	(Asm_simp_tac 1),
   9.189  	(dtac spec 1),
   9.190  	(rtac mp 1),
   9.191  	(atac 1),
    10.1 --- a/src/HOLCF/HOLCF.ML	Wed Oct 04 13:12:14 1995 +0100
    10.2 +++ b/src/HOLCF/HOLCF.ML	Wed Oct 04 14:01:44 1995 +0100
    10.3 @@ -6,16 +6,5 @@
    10.4  
    10.5  open HOLCF;
    10.6  
    10.7 -val HOLCF_ss = ccc1_ss 
    10.8 -		addsimps one_when 
    10.9 -		addsimps dist_less_one
   10.10 -		addsimps dist_eq_one 
   10.11 -		addsimps dist_less_tr
   10.12 -		addsimps dist_eq_tr
   10.13 -		addsimps tr_when
   10.14 -		addsimps andalso_thms
   10.15 -		addsimps orelse_thms
   10.16 -                addsimps neg_thms
   10.17 -		addsimps ifte_thms;
   10.18 -
   10.19 -
   10.20 +Addsimps (one_when @ dist_less_one @ dist_eq_one @ dist_less_tr @ dist_eq_tr
   10.21 +          @ tr_when @ andalso_thms @ orelse_thms @ neg_thms @ ifte_thms);
    11.1 --- a/src/HOLCF/Lift1.ML	Wed Oct 04 13:12:14 1995 +0100
    11.2 +++ b/src/HOLCF/Lift1.ML	Wed Oct 04 14:01:44 1995 +0100
    11.3 @@ -84,7 +84,7 @@
    11.4  	(rtac refl 1)
    11.5  	]);
    11.6  
    11.7 -val Lift_ss = Cfun_ss addsimps [Ilift1,Ilift2];
    11.8 +Addsimps [Ilift1,Ilift2];
    11.9  
   11.10  qed_goalw "less_lift1a"  Lift1.thy [less_lift_def,UU_lift_def]
   11.11  	"less_lift(UU_lift)(z)"
    12.1 --- a/src/HOLCF/Lift2.ML	Wed Oct 04 13:12:14 1995 +0100
    12.2 +++ b/src/HOLCF/Lift2.ML	Wed Oct 04 14:01:44 1995 +0100
    12.3 @@ -55,8 +55,8 @@
    12.4  	(rtac (less_fun RS iffD2) 1),
    12.5  	(strip_tac 1),
    12.6  	(res_inst_tac [("p","xa")] liftE 1),
    12.7 -	(asm_simp_tac Lift_ss 1),
    12.8 -	(asm_simp_tac Lift_ss 1),
    12.9 +	(Asm_simp_tac 1),
   12.10 +	(Asm_simp_tac 1),
   12.11  	(etac monofun_cfun_fun 1)
   12.12  	]);
   12.13  
   12.14 @@ -65,14 +65,14 @@
   12.15  	[
   12.16  	(strip_tac 1),
   12.17  	(res_inst_tac [("p","x")] liftE 1),
   12.18 -	(asm_simp_tac Lift_ss 1),
   12.19 -	(asm_simp_tac Lift_ss 1),
   12.20 +	(Asm_simp_tac 1),
   12.21 +	(Asm_simp_tac 1),
   12.22  	(res_inst_tac [("p","y")] liftE 1),
   12.23  	(hyp_subst_tac 1),
   12.24  	(rtac notE 1),
   12.25  	(rtac less_lift2b 1),
   12.26  	(atac 1),
   12.27 -	(asm_simp_tac Lift_ss 1),
   12.28 +	(Asm_simp_tac 1),
   12.29  	(rtac monofun_cfun_arg 1),
   12.30  	(hyp_subst_tac 1),
   12.31  	(etac (less_lift2c  RS iffD1) 1)
   12.32 @@ -87,7 +87,7 @@
   12.33   (fn prems =>
   12.34  	[
   12.35  	(cut_facts_tac prems 1),
   12.36 -	(asm_simp_tac Lift_ss 1)
   12.37 +	(Asm_simp_tac 1)
   12.38  	]);
   12.39  
   12.40  (* ------------------------------------------------------------------------ *)
    13.1 --- a/src/HOLCF/Lift3.ML	Wed Oct 04 13:12:14 1995 +0100
    13.2 +++ b/src/HOLCF/Lift3.ML	Wed Oct 04 14:01:44 1995 +0100
    13.3 @@ -44,7 +44,7 @@
    13.4  	(atac 1),
    13.5  	(rtac (monofun_Ilift2 RS ch2ch_monofun) 1),
    13.6  	(etac (monofun_Iup RS ch2ch_monofun) 1),
    13.7 -	(asm_simp_tac Lift_ss 1)
    13.8 +	(Asm_simp_tac 1)
    13.9  	]);
   13.10  
   13.11  qed_goal "cont_Iup" Lift3.thy "cont(Iup)"
   13.12 @@ -70,9 +70,9 @@
   13.13  	(etac (monofun_Ilift1 RS ch2ch_monofun) 2),
   13.14  	(rtac ext 1),
   13.15  	(res_inst_tac [("p","x")] liftE 1),
   13.16 -	(asm_simp_tac Lift_ss 1),
   13.17 +	(Asm_simp_tac 1),
   13.18  	(rtac (lub_const RS thelubI RS sym) 1),
   13.19 -	(asm_simp_tac Lift_ss 1),
   13.20 +	(Asm_simp_tac 1),
   13.21  	(etac contlub_cfun_fun 1)
   13.22  	]);
   13.23  
   13.24 @@ -86,16 +86,16 @@
   13.25  	(rtac (thelub_lift1a RS ssubst) 2),
   13.26  	(atac 2),
   13.27  	(atac 2),
   13.28 -	(asm_simp_tac Lift_ss 2),
   13.29 +	(Asm_simp_tac 2),
   13.30  	(rtac (thelub_lift1b RS ssubst) 3),
   13.31  	(atac 3),
   13.32  	(atac 3),
   13.33  	(fast_tac HOL_cs 1),
   13.34 -	(asm_simp_tac Lift_ss 2),
   13.35 +	(Asm_simp_tac 2),
   13.36  	(rtac (chain_UU_I_inverse RS sym) 2),
   13.37  	(rtac allI 2),
   13.38  	(res_inst_tac [("p","Y(i)")] liftE 2),
   13.39 -	(asm_simp_tac Lift_ss 2),
   13.40 +	(Asm_simp_tac 2),
   13.41  	(rtac notE 2),
   13.42  	(dtac spec 2),
   13.43  	(etac spec 2),
   13.44 @@ -117,7 +117,7 @@
   13.45  	(rtac exI 1),
   13.46  	(strip_tac 1),
   13.47  	(res_inst_tac [("p","Y(i)")] liftE 1),
   13.48 -	(asm_simp_tac Lift_ss 2),
   13.49 +	(Asm_simp_tac 2),
   13.50  	(res_inst_tac [("P","Y(i) = UU")] notE 1),
   13.51  	(fast_tac HOL_cs 1),
   13.52  	(rtac (inst_lift_pcpo RS ssubst) 1),
   13.53 @@ -148,7 +148,7 @@
   13.54  qed_goalw "Exh_Lift1" Lift3.thy [up_def] "z = UU | (? x. z = up`x)"
   13.55   (fn prems =>
   13.56  	[
   13.57 -	(simp_tac (Lift_ss addsimps [cont_Iup]) 1),
   13.58 +	(simp_tac (!simpset addsimps [cont_Iup]) 1),
   13.59  	(rtac (inst_lift_pcpo RS ssubst) 1),
   13.60  	(rtac Exh_Lift 1)
   13.61  	]);
   13.62 @@ -159,14 +159,14 @@
   13.63  	(cut_facts_tac prems 1),
   13.64  	(rtac inject_Iup 1),
   13.65  	(etac box_equals 1),
   13.66 -	(simp_tac (Lift_ss addsimps [cont_Iup]) 1),
   13.67 -	(simp_tac (Lift_ss addsimps [cont_Iup]) 1)
   13.68 +	(simp_tac (!simpset addsimps [cont_Iup]) 1),
   13.69 +	(simp_tac (!simpset addsimps [cont_Iup]) 1)
   13.70  	]);
   13.71  
   13.72  qed_goalw "defined_up" Lift3.thy [up_def] " up`x ~= UU"
   13.73   (fn prems =>
   13.74  	[
   13.75 -	(simp_tac (Lift_ss addsimps [cont_Iup]) 1),
   13.76 +	(simp_tac (!simpset addsimps [cont_Iup]) 1),
   13.77  	(rtac defined_Iup2 1)
   13.78  	]);
   13.79  
   13.80 @@ -178,7 +178,7 @@
   13.81  	(resolve_tac prems 1),
   13.82  	(etac (inst_lift_pcpo RS ssubst) 1),
   13.83  	(resolve_tac (tl prems) 1),
   13.84 -	(asm_simp_tac (Lift_ss addsimps [cont_Iup]) 1)
   13.85 +	(asm_simp_tac (!simpset addsimps [cont_Iup]) 1)
   13.86  	]);
   13.87  
   13.88  
   13.89 @@ -192,7 +192,7 @@
   13.90  	(rtac (beta_cfun RS ssubst) 1),
   13.91  	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
   13.92  		cont_Ilift2,cont2cont_CF1L]) 1)),
   13.93 -	(simp_tac (Lift_ss addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
   13.94 +	(simp_tac (!simpset addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
   13.95  	]);
   13.96  
   13.97  qed_goalw "lift2" Lift3.thy [up_def,lift_def] "lift`f`(up`x)=f`x"
   13.98 @@ -205,13 +205,13 @@
   13.99  		cont_Ilift2,cont2cont_CF1L]) 1)),
  13.100  	(rtac (beta_cfun RS ssubst) 1),
  13.101  	(rtac cont_Ilift2 1),
  13.102 -	(simp_tac (Lift_ss addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
  13.103 +	(simp_tac (!simpset addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
  13.104  	]);
  13.105  
  13.106  qed_goalw "less_lift4b" Lift3.thy [up_def,lift_def] "~ up`x << UU"
  13.107   (fn prems =>
  13.108  	[
  13.109 -	(simp_tac (Lift_ss addsimps [cont_Iup]) 1),
  13.110 +	(simp_tac (!simpset addsimps [cont_Iup]) 1),
  13.111  	(rtac less_lift3b 1)
  13.112  	]);
  13.113  
  13.114 @@ -219,7 +219,7 @@
  13.115  	 "(up`x << up`y) = (x<<y)"
  13.116   (fn prems =>
  13.117  	[
  13.118 -	(simp_tac (Lift_ss addsimps [cont_Iup]) 1),
  13.119 +	(simp_tac (!simpset addsimps [cont_Iup]) 1),
  13.120  	(rtac less_lift2c 1)
  13.121  	]);
  13.122  
  13.123 @@ -247,7 +247,7 @@
  13.124  	(rtac exI 1),
  13.125  	(etac box_equals 1),
  13.126  	(rtac refl 1),
  13.127 -	(simp_tac (Lift_ss addsimps [cont_Iup]) 1)
  13.128 +	(simp_tac (!simpset addsimps [cont_Iup]) 1)
  13.129  	]);
  13.130  
  13.131  
  13.132 @@ -268,7 +268,7 @@
  13.133  	(dtac notnotD 1),
  13.134  	(etac box_equals 1),
  13.135  	(rtac refl 1),
  13.136 -	(simp_tac (Lift_ss addsimps [cont_Iup]) 1)
  13.137 +	(simp_tac (!simpset addsimps [cont_Iup]) 1)
  13.138  	]);
  13.139  
  13.140  
  13.141 @@ -338,8 +338,8 @@
  13.142   (fn prems =>
  13.143  	[
  13.144  	(res_inst_tac [("p","x")] liftE1 1),
  13.145 -	(asm_simp_tac (Cfun_ss addsimps [lift1,lift2]) 1),
  13.146 -	(asm_simp_tac (Cfun_ss addsimps [lift1,lift2]) 1)
  13.147 +	(asm_simp_tac (!simpset addsimps [lift1,lift2]) 1),
  13.148 +	(asm_simp_tac (!simpset addsimps [lift1,lift2]) 1)
  13.149  	]);
  13.150  
  13.151  (* ------------------------------------------------------------------------ *)
    14.1 --- a/src/HOLCF/One.ML	Wed Oct 04 13:12:14 1995 +0100
    14.2 +++ b/src/HOLCF/One.ML	Wed Oct 04 14:01:44 1995 +0100
    14.3 @@ -74,10 +74,10 @@
    14.4  	(rtac allI 1),
    14.5  	(rtac allI 1),
    14.6  	(res_inst_tac [("p","x")] oneE 1),
    14.7 -	(asm_simp_tac ccc1_ss  1),
    14.8 +	(Asm_simp_tac 1),
    14.9  	(res_inst_tac [("p","y")] oneE 1),
   14.10 -	(asm_simp_tac (ccc1_ss addsimps dist_less_one) 1),
   14.11 -	(asm_simp_tac ccc1_ss  1)
   14.12 +	(asm_simp_tac (!simpset addsimps dist_less_one) 1),
   14.13 +	(Asm_simp_tac 1)
   14.14  	]);
   14.15  
   14.16  
   14.17 @@ -89,7 +89,7 @@
   14.18  fun prover s =  prove_goalw One.thy [one_when_def,one_def] s
   14.19   (fn prems =>
   14.20  	[
   14.21 -	(simp_tac (ccc1_ss addsimps [(rep_one_iso ),
   14.22 +	(simp_tac (!simpset addsimps [(rep_one_iso ),
   14.23  	(abs_one_iso RS allI) RS ((rep_one_iso RS allI) 
   14.24  	RS iso_strict) RS conjunct1] )1)
   14.25  	]);
    15.1 --- a/src/HOLCF/Pcpo.ML	Wed Oct 04 13:12:14 1995 +0100
    15.2 +++ b/src/HOLCF/Pcpo.ML	Wed Oct 04 14:01:44 1995 +0100
    15.3 @@ -105,7 +105,7 @@
    15.4  	(atac 1),
    15.5  	(res_inst_tac [("s","Y(Suc(x))"),("t","X(Suc(x))")] subst 1),
    15.6  	(rtac sym 1),
    15.7 -	(asm_simp_tac nat_ss 1),
    15.8 +	(Asm_simp_tac 1),
    15.9  	(rtac is_ub_thelub 1),
   15.10  	(resolve_tac prems 1)
   15.11  	]);
    16.1 --- a/src/HOLCF/Porder.ML	Wed Oct 04 13:12:14 1995 +0100
    16.2 +++ b/src/HOLCF/Porder.ML	Wed Oct 04 14:01:44 1995 +0100
    16.3 @@ -252,7 +252,7 @@
    16.4  	[
    16.5  	(rtac (inst_void_po RS ssubst) 1),
    16.6  	(rewrite_goals_tac [less_void_def]),
    16.7 -	(simp_tac (HOL_ss addsimps [unique_void]) 1)
    16.8 +	(simp_tac (!simpset addsimps [unique_void]) 1)
    16.9  	]);
   16.10  
   16.11  (* ------------------------------------------------------------------------ *)
   16.12 @@ -267,7 +267,7 @@
   16.13  	(strip_tac 1),
   16.14  	(rtac (inst_void_po RS ssubst) 1),
   16.15  	(rewrite_goals_tac [less_void_def]),
   16.16 -	(simp_tac (HOL_ss addsimps [unique_void]) 1),
   16.17 +	(simp_tac (!simpset addsimps [unique_void]) 1),
   16.18  	(strip_tac 1),
   16.19  	(rtac minimal_void 1)
   16.20  	]);
   16.21 @@ -341,8 +341,8 @@
   16.22  	(rtac is_chainI 1),
   16.23  	(rtac allI 1),
   16.24  	(nat_ind_tac "i" 1),
   16.25 -	(asm_simp_tac nat_ss 1),
   16.26 -	(asm_simp_tac nat_ss 1),
   16.27 +	(Asm_simp_tac 1),
   16.28 +	(Asm_simp_tac 1),
   16.29  	(rtac refl_less 1)
   16.30  	]);
   16.31  
   16.32 @@ -353,8 +353,8 @@
   16.33  	(cut_facts_tac prems 1),
   16.34  	(rtac allI 1),
   16.35  	(nat_ind_tac "j" 1),
   16.36 -	(asm_simp_tac nat_ss 1),
   16.37 -	(asm_simp_tac nat_ss 1)
   16.38 +	(Asm_simp_tac 1),
   16.39 +	(Asm_simp_tac 1)
   16.40  	]);
   16.41  
   16.42  qed_goal "lub_bin_chain" Porder.thy 
   16.43 @@ -365,7 +365,7 @@
   16.44  	(rtac lub_finch1 2),
   16.45  	(etac bin_chain 2),
   16.46  	(etac bin_chainmax 2),
   16.47 -	(simp_tac nat_ss  1)
   16.48 +	(Simp_tac  1)
   16.49  	]);
   16.50  
   16.51  (* ------------------------------------------------------------------------ *)
    17.1 --- a/src/HOLCF/ROOT.ML	Wed Oct 04 13:12:14 1995 +0100
    17.2 +++ b/src/HOLCF/ROOT.ML	Wed Oct 04 14:01:44 1995 +0100
    17.3 @@ -13,58 +13,7 @@
    17.4  
    17.5  init_thy_reader();
    17.6  
    17.7 -
    17.8 -use_thy "Holcfb";
    17.9 -use_thy "Void";
   17.10 -
   17.11 -use_thy "Porder0";
   17.12 -use_thy "Porder";
   17.13 -
   17.14 -use_thy "Pcpo";
   17.15 -
   17.16 -use_thy "Fun1";
   17.17 -use_thy "Fun2";
   17.18 -use_thy "Fun3";
   17.19 -
   17.20 -use_thy "Cont";
   17.21 -
   17.22 -use_thy "Cfun1";
   17.23 -use_thy "Cfun2";
   17.24 -use_thy "Cfun3";
   17.25 -
   17.26 -use_thy "Cprod1";
   17.27 -use_thy "Cprod2";
   17.28 -use_thy "Cprod3";
   17.29 -
   17.30 -use_thy "Sprod0";
   17.31 -use_thy "Sprod1"; 
   17.32 -use_thy "Sprod2"; 
   17.33 -use_thy "Sprod3"; 
   17.34 -
   17.35 -use_thy "Ssum0";
   17.36 -use_thy "Ssum1";
   17.37 -use_thy "Ssum2";
   17.38 -use_thy "Ssum3";
   17.39 -
   17.40 -use_thy "Lift1";
   17.41 -use_thy "Lift2";
   17.42 -use_thy "Lift3";
   17.43 -
   17.44  use_thy "Fix";
   17.45 -
   17.46 -use_thy "ccc1";
   17.47 -use_thy "One";
   17.48 -use_thy "Tr1";
   17.49 -use_thy "Tr2";
   17.50 - 
   17.51 -use_thy "HOLCF";
   17.52 -
   17.53 -use_thy "Dnat";
   17.54 -use_thy "Dnat2";
   17.55 -
   17.56 -use_thy "Stream";
   17.57 -use_thy "Stream2";
   17.58 -
   17.59  use_thy "Dlist";
   17.60  
   17.61  use "../Pure/install_pp.ML";
    18.1 --- a/src/HOLCF/Sprod0.ML	Wed Oct 04 13:12:14 1995 +0100
    18.2 +++ b/src/HOLCF/Sprod0.ML	Wed Oct 04 14:01:44 1995 +0100
    18.3 @@ -340,10 +340,8 @@
    18.4  (* instantiate the simplifier                                               *)
    18.5  (* ------------------------------------------------------------------------ *)
    18.6  
    18.7 -val Sprod_ss = 
    18.8 -	HOL_ss 
    18.9 -	addsimps [strict_Isfst1,strict_Isfst2,strict_Issnd1,strict_Issnd2,
   18.10 -		 Isfst2,Issnd2];
   18.11 +Addsimps [strict_Isfst1,strict_Isfst2,strict_Issnd1,strict_Issnd2,
   18.12 +	  Isfst2,Issnd2];
   18.13  
   18.14  
   18.15  qed_goal "defined_IsfstIssnd" Sprod0.thy 
   18.16 @@ -355,8 +353,8 @@
   18.17  	(contr_tac 1),
   18.18  	(hyp_subst_tac 1),
   18.19  	(rtac conjI 1),
   18.20 -	(asm_simp_tac Sprod_ss 1),
   18.21 -	(asm_simp_tac Sprod_ss 1)
   18.22 +	(Asm_simp_tac 1),
   18.23 +	(Asm_simp_tac 1)
   18.24  	]);
   18.25  
   18.26  
   18.27 @@ -369,10 +367,10 @@
   18.28  (fn prems =>
   18.29  	[
   18.30  	(res_inst_tac [("z1","z")] (Exh_Sprod RS disjE) 1),
   18.31 -	(asm_simp_tac Sprod_ss 1),
   18.32 +	(Asm_simp_tac 1),
   18.33  	(etac exE 1),
   18.34  	(etac exE 1),
   18.35 -	(asm_simp_tac Sprod_ss 1)
   18.36 +	(Asm_simp_tac 1)
   18.37  	]);
   18.38  
   18.39  
    19.1 --- a/src/HOLCF/Sprod1.ML	Wed Oct 04 13:12:14 1995 +0100
    19.2 +++ b/src/HOLCF/Sprod1.ML	Wed Oct 04 14:01:44 1995 +0100
    19.3 @@ -18,7 +18,7 @@
    19.4   (fn prems =>
    19.5  	[
    19.6  	(cut_facts_tac prems 1),
    19.7 -	(asm_simp_tac HOL_ss 1)
    19.8 +	(Asm_simp_tac 1)
    19.9  	]);
   19.10  
   19.11  qed_goalw "less_sprod1b" Sprod1.thy [less_sprod_def]
   19.12 @@ -27,7 +27,7 @@
   19.13   (fn prems =>
   19.14  	[
   19.15  	(cut_facts_tac prems 1),
   19.16 -	(asm_simp_tac HOL_ss 1)
   19.17 +	(Asm_simp_tac 1)
   19.18  	]);
   19.19  
   19.20  qed_goal "less_sprod2a" Sprod1.thy
   19.21 @@ -45,7 +45,7 @@
   19.22  	(fast_tac HOL_cs 1),
   19.23  	(fast_tac HOL_cs 1),
   19.24  	(res_inst_tac [("s","Isfst(Ispair UU UU)"),("t","UU")] subst 1),
   19.25 -	(simp_tac Sprod_ss 1),
   19.26 +	(Simp_tac 1),
   19.27  	(rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct1) 1),
   19.28  	(REPEAT (fast_tac HOL_cs 1))
   19.29  	]);
   19.30 @@ -69,21 +69,21 @@
   19.31  	[
   19.32  	(rtac conjI 1),
   19.33  	(res_inst_tac [("s","Isfst(Ispair xa ya)"),("t","xa")] subst 1),
   19.34 -	(simp_tac (Sprod_ss addsimps prems)1),
   19.35 +	(simp_tac (!simpset addsimps prems)1),
   19.36  	(res_inst_tac [("s","Isfst(Ispair x y)"),("t","x")] subst 1),
   19.37 -	(simp_tac (Sprod_ss addsimps prems)1),
   19.38 +	(simp_tac (!simpset addsimps prems)1),
   19.39  	(rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct1) 1),
   19.40  	(resolve_tac prems 1),
   19.41  	(resolve_tac prems 1),
   19.42 -	(simp_tac (Sprod_ss addsimps prems)1),
   19.43 +	(simp_tac (!simpset addsimps prems)1),
   19.44  	(res_inst_tac [("s","Issnd(Ispair xa ya)"),("t","ya")] subst 1),
   19.45 -	(simp_tac (Sprod_ss addsimps prems)1),
   19.46 +	(simp_tac (!simpset addsimps prems)1),
   19.47  	(res_inst_tac [("s","Issnd(Ispair x y)"),("t","y")] subst 1),
   19.48 -	(simp_tac (Sprod_ss addsimps prems)1),
   19.49 +	(simp_tac (!simpset addsimps prems)1),
   19.50  	(rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct2) 1),
   19.51  	(resolve_tac prems 1),
   19.52  	(resolve_tac prems 1),
   19.53 -	(simp_tac (Sprod_ss addsimps prems)1)
   19.54 +	(simp_tac (!simpset addsimps prems)1)
   19.55  	]);
   19.56  
   19.57  (* ------------------------------------------------------------------------ *)
   19.58 @@ -123,11 +123,11 @@
   19.59  	(hyp_subst_tac 1),
   19.60  	(res_inst_tac [("x1","x"),("y1","xa"),("x","y"),("y","ya")] (arg_cong RS cong) 1),
   19.61  	(rtac antisym_less 1),
   19.62 -	(asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct1]) 1),
   19.63 -	(asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct1]) 1),
   19.64 +	(asm_simp_tac (!simpset addsimps [less_sprod2c RS conjunct1]) 1),
   19.65 +	(asm_simp_tac (!simpset addsimps [less_sprod2c RS conjunct1]) 1),
   19.66  	(rtac antisym_less 1),
   19.67 -	(asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct2]) 1),
   19.68 -	(asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct2]) 1)
   19.69 +	(asm_simp_tac (!simpset addsimps [less_sprod2c RS conjunct2]) 1),
   19.70 +	(asm_simp_tac (!simpset addsimps [less_sprod2c RS conjunct2]) 1)
   19.71  	]);
   19.72  
   19.73  qed_goal "trans_less_sprod" Sprod1.thy 
    20.1 --- a/src/HOLCF/Sprod3.ML	Wed Oct 04 13:12:14 1995 +0100
    20.2 +++ b/src/HOLCF/Sprod3.ML	Wed Oct 04 14:01:44 1995 +0100
    20.3 @@ -28,7 +28,7 @@
    20.4  	(rtac (monofun_Ispair1 RS ch2ch_monofun) 1),
    20.5  	(atac 1),
    20.6  	(rtac allI 1),
    20.7 -	(asm_simp_tac Sprod_ss 1),
    20.8 +	(Asm_simp_tac 1),
    20.9  	(rtac sym 1),
   20.10  	(rtac lub_chain_maxelem 1),
   20.11  	(res_inst_tac [("P","%j.~Y(j)=UU")] exE 1),
   20.12 @@ -41,12 +41,10 @@
   20.13  	(etac Issnd2 1),
   20.14  	(rtac allI 1),
   20.15  	(res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1),
   20.16 -	(asm_simp_tac Sprod_ss  1),
   20.17 -	(rtac refl_less 1),
   20.18 +	(Asm_simp_tac 1),
   20.19  	(res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
   20.20  	(etac sym 1),
   20.21 -	(asm_simp_tac Sprod_ss  1),
   20.22 -	(rtac minimal 1)
   20.23 +	(Asm_simp_tac 1)
   20.24  	]);
   20.25  
   20.26  qed_goal "sprod3_lemma2" Sprod3.thy 
   20.27 @@ -65,7 +63,7 @@
   20.28  	(rtac disjI1 1),
   20.29  	(rtac chain_UU_I_inverse 1),
   20.30  	(rtac allI 1),
   20.31 -	(asm_simp_tac Sprod_ss  1),
   20.32 +	(Asm_simp_tac  1),
   20.33  	(etac (chain_UU_I RS spec) 1),
   20.34  	(atac 1)
   20.35  	]);
   20.36 @@ -87,7 +85,7 @@
   20.37  	(rtac disjI1 1),
   20.38  	(rtac chain_UU_I_inverse 1),
   20.39  	(rtac allI 1),
   20.40 -	(simp_tac Sprod_ss  1)
   20.41 +	(Simp_tac  1)
   20.42  	]);
   20.43  
   20.44  
   20.45 @@ -138,19 +136,17 @@
   20.46  	(etac Isfst2 1),
   20.47  	(rtac allI 1),
   20.48  	(res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1),
   20.49 -	(asm_simp_tac Sprod_ss 1),
   20.50 -	(rtac refl_less 1),
   20.51 +	(Asm_simp_tac 1),
   20.52  	(res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
   20.53  	(etac sym 1),
   20.54 -	(asm_simp_tac Sprod_ss  1),
   20.55 -	(rtac minimal 1),
   20.56 +	(Asm_simp_tac  1),
   20.57  	(rtac lub_equal 1),
   20.58  	(atac 1),
   20.59  	(rtac (monofun_Issnd RS ch2ch_monofun) 1),
   20.60  	(rtac (monofun_Ispair2 RS ch2ch_monofun) 1),
   20.61  	(atac 1),
   20.62  	(rtac allI 1),
   20.63 -	(asm_simp_tac Sprod_ss 1)
   20.64 +	(Asm_simp_tac 1)
   20.65  	]);
   20.66  
   20.67  qed_goal "sprod3_lemma5" Sprod3.thy 
   20.68 @@ -169,7 +165,7 @@
   20.69  	(rtac disjI2 1),
   20.70  	(rtac chain_UU_I_inverse 1),
   20.71  	(rtac allI 1),
   20.72 -	(asm_simp_tac Sprod_ss  1),
   20.73 +	(Asm_simp_tac  1),
   20.74  	(etac (chain_UU_I RS spec) 1),
   20.75  	(atac 1)
   20.76  	]);
   20.77 @@ -190,7 +186,7 @@
   20.78  	(rtac disjI1 1),
   20.79  	(rtac chain_UU_I_inverse 1),
   20.80  	(rtac allI 1),
   20.81 -	(simp_tac Sprod_ss  1)
   20.82 +	(Simp_tac 1)
   20.83  	]);
   20.84  
   20.85  qed_goal "contlub_Ispair2" Sprod3.thy "contlub(Ispair(x))"
   20.86 @@ -241,12 +237,12 @@
   20.87  	(atac 1),
   20.88  	(res_inst_tac [("Q","lub(range(%i. Issnd(Y(i))))=UU")]	
   20.89  		(excluded_middle RS disjE) 1),
   20.90 -	(asm_simp_tac Sprod_ss  1),
   20.91 +	(Asm_simp_tac  1),
   20.92  	(res_inst_tac [("s","UU"),("t","lub(range(%i. Issnd(Y(i))))")]
   20.93  		ssubst 1),
   20.94  	(atac 1),
   20.95  	(rtac trans 1),
   20.96 -	(asm_simp_tac Sprod_ss  1),
   20.97 +	(Asm_simp_tac  1),
   20.98  	(rtac sym 1),
   20.99  	(rtac chain_UU_I_inverse 1),
  20.100  	(rtac allI 1),
  20.101 @@ -270,11 +266,11 @@
  20.102  	(atac 1),
  20.103  	(res_inst_tac [("Q","lub(range(%i. Isfst(Y(i))))=UU")]
  20.104  	 (excluded_middle RS disjE) 1),
  20.105 -	(asm_simp_tac Sprod_ss  1),
  20.106 +	(Asm_simp_tac  1),
  20.107  	(res_inst_tac [("s","UU"),("t","lub(range(%i. Isfst(Y(i))))")] 
  20.108  		ssubst 1),
  20.109  	(atac 1),
  20.110 -	(asm_simp_tac Sprod_ss  1),
  20.111 +	(Asm_simp_tac  1),
  20.112  	(rtac sym 1),
  20.113  	(rtac chain_UU_I_inverse 1),
  20.114  	(rtac allI 1),
  20.115 @@ -679,10 +675,8 @@
  20.116  (* install simplifier for Sprod                                             *)
  20.117  (* ------------------------------------------------------------------------ *)
  20.118  
  20.119 -val Sprod_rews = [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2,
  20.120 -		strict_ssnd1,strict_ssnd2,sfst2,ssnd2,
  20.121 -		ssplit1,ssplit2];
  20.122 -
  20.123 -val Sprod_ss = Cfun_ss addsimps Sprod_rews;
  20.124 +Addsimps [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2,
  20.125 +	  strict_ssnd1,strict_ssnd2,sfst2,ssnd2,
  20.126 +	  ssplit1,ssplit2];
  20.127  
  20.128  
    21.1 --- a/src/HOLCF/Ssum0.ML	Wed Oct 04 13:12:14 1995 +0100
    21.2 +++ b/src/HOLCF/Ssum0.ML	Wed Oct 04 14:01:44 1995 +0100
    21.3 @@ -388,7 +388,6 @@
    21.4  (* instantiate the simplifier                                               *)
    21.5  (* ------------------------------------------------------------------------ *)
    21.6  
    21.7 -val Ssum_ss = Cfun_ss addsimps 
    21.8 -		[(strict_IsinlIsinr RS sym),Iwhen1,Iwhen2,Iwhen3];
    21.9 +Addsimps [(strict_IsinlIsinr RS sym),Iwhen1,Iwhen2,Iwhen3];
   21.10  
   21.11  
    22.1 --- a/src/HOLCF/Ssum1.ML	Wed Oct 04 13:12:14 1995 +0100
    22.2 +++ b/src/HOLCF/Ssum1.ML	Wed Oct 04 14:01:44 1995 +0100
    22.3 @@ -62,7 +62,7 @@
    22.4  	(etac conjE 1),
    22.5  	(UU_left "x"),
    22.6  	(UU_right "v"),
    22.7 -	(simp_tac Cfun_ss 1),
    22.8 +	(Simp_tac 1),
    22.9  	(rtac conjI 1),
   22.10  	(strip_tac 1),
   22.11  	(etac conjE 1),
   22.12 @@ -77,7 +77,7 @@
   22.13  	(etac conjE 1),
   22.14  	(UU_left "x"),
   22.15  	(UU_right "v"),
   22.16 -	(simp_tac Cfun_ss 1)
   22.17 +	(Simp_tac 1)
   22.18  	]);
   22.19  
   22.20  
   22.21 @@ -98,7 +98,7 @@
   22.22  	(etac conjE 1),
   22.23  	(UU_right "x"),
   22.24  	(UU_left "u"),
   22.25 -	(simp_tac Cfun_ss 1),
   22.26 +	(Simp_tac 1),
   22.27  	(rtac conjI 1),
   22.28  	(strip_tac 1),
   22.29  	(etac conjE 1),
   22.30 @@ -110,7 +110,7 @@
   22.31  	(etac conjE 1),
   22.32  	(UU_right "x"),
   22.33  	(UU_left "u"),
   22.34 -	(simp_tac Cfun_ss 1),
   22.35 +	(Simp_tac 1),
   22.36  	(strip_tac 1),
   22.37  	(etac conjE 1),
   22.38  	(eq_right "x" "v"),
   22.39 @@ -144,7 +144,7 @@
   22.40  	(etac conjE 1),
   22.41  	(UU_left "x"),
   22.42  	(UU_right "v"),
   22.43 -	(simp_tac Cfun_ss 1),
   22.44 +	(Simp_tac 1),
   22.45  	(rtac conjI 1),
   22.46  	(strip_tac 1),
   22.47  	(etac conjE 1),
   22.48 @@ -154,7 +154,7 @@
   22.49  	(etac conjE 1),
   22.50  	(UU_left "x"),
   22.51  	(UU_right "v"),
   22.52 -	(simp_tac Cfun_ss 1),
   22.53 +	(Simp_tac 1),
   22.54  	(dtac conjunct2 1),
   22.55  	(dtac conjunct2 1),
   22.56  	(dtac conjunct1 1),
   22.57 @@ -183,7 +183,7 @@
   22.58  	(etac conjE 1),
   22.59  	(UU_right "x"),
   22.60  	(UU_left "u"),
   22.61 -	(simp_tac Cfun_ss 1),
   22.62 +	(Simp_tac 1),
   22.63  	(rtac conjI 1),
   22.64  	(strip_tac 1),
   22.65  	(etac conjE 1),
   22.66 @@ -199,7 +199,7 @@
   22.67  	(etac conjE 1),
   22.68  	(UU_right "x"),
   22.69  	(UU_left "u"),
   22.70 -	(simp_tac HOL_ss 1),
   22.71 +	(Simp_tac 1),
   22.72  	(strip_tac 1),
   22.73  	(etac conjE 1),
   22.74  	(eq_right "x" "v"),
    23.1 --- a/src/HOLCF/Ssum2.ML	Wed Oct 04 13:12:14 1995 +0100
    23.2 +++ b/src/HOLCF/Ssum2.ML	Wed Oct 04 14:01:44 1995 +0100
    23.3 @@ -97,10 +97,10 @@
    23.4  	(strip_tac 1),
    23.5  	(res_inst_tac [("p","xb")] IssumE 1),
    23.6  	(hyp_subst_tac 1),
    23.7 -	(asm_simp_tac Ssum_ss 1),
    23.8 -	(asm_simp_tac Ssum_ss 1),
    23.9 +	(Asm_simp_tac 1),
   23.10 +	(Asm_simp_tac 1),
   23.11  	(etac monofun_cfun_fun 1),
   23.12 -	(asm_simp_tac Ssum_ss 1)
   23.13 +	(Asm_simp_tac 1)
   23.14  	]);
   23.15  
   23.16  qed_goalw "monofun_Iwhen2" Ssum2.thy [monofun] "monofun(Iwhen(f))"
   23.17 @@ -111,9 +111,9 @@
   23.18  	(strip_tac 1),
   23.19  	(res_inst_tac [("p","xa")] IssumE 1),
   23.20  	(hyp_subst_tac 1),
   23.21 -	(asm_simp_tac Ssum_ss 1),
   23.22 -	(asm_simp_tac Ssum_ss 1),
   23.23 -	(asm_simp_tac Ssum_ss 1),
   23.24 +	(Asm_simp_tac 1),
   23.25 +	(Asm_simp_tac 1),
   23.26 +	(Asm_simp_tac 1),
   23.27  	(etac monofun_cfun_fun 1)
   23.28  	]);
   23.29  
   23.30 @@ -123,36 +123,36 @@
   23.31  	(strip_tac 1),
   23.32  	(res_inst_tac [("p","x")] IssumE 1),
   23.33  	(hyp_subst_tac 1),
   23.34 -	(asm_simp_tac Ssum_ss 1),
   23.35 +	(Asm_simp_tac 1),
   23.36  	(hyp_subst_tac 1),
   23.37  	(res_inst_tac [("p","y")] IssumE 1),
   23.38  	(hyp_subst_tac 1),
   23.39 -	(asm_simp_tac Ssum_ss 1),
   23.40 +	(Asm_simp_tac 1),
   23.41  	(res_inst_tac  [("P","xa=UU")] notE 1),
   23.42  	(atac 1),
   23.43  	(rtac UU_I 1),
   23.44  	(rtac (less_ssum3a  RS iffD1) 1),
   23.45  	(atac 1),
   23.46  	(hyp_subst_tac 1),
   23.47 -	(asm_simp_tac Ssum_ss 1),
   23.48 +	(Asm_simp_tac 1),
   23.49  	(rtac monofun_cfun_arg 1),
   23.50  	(etac (less_ssum3a  RS iffD1) 1),
   23.51  	(hyp_subst_tac 1),
   23.52  	(res_inst_tac [("s","UU"),("t","xa")] subst 1),
   23.53  	(etac (less_ssum3c  RS iffD1 RS sym) 1),
   23.54 -	(asm_simp_tac Ssum_ss 1),
   23.55 +	(Asm_simp_tac 1),
   23.56  	(hyp_subst_tac 1),
   23.57  	(res_inst_tac [("p","y")] IssumE 1),
   23.58  	(hyp_subst_tac 1),
   23.59  	(res_inst_tac [("s","UU"),("t","ya")] subst 1),
   23.60  	(etac (less_ssum3d  RS iffD1 RS sym) 1),
   23.61 -	(asm_simp_tac Ssum_ss 1),
   23.62 +	(Asm_simp_tac 1),
   23.63  	(hyp_subst_tac 1),
   23.64  	(res_inst_tac [("s","UU"),("t","ya")] subst 1),
   23.65  	(etac (less_ssum3d  RS iffD1 RS sym) 1),
   23.66 -	(asm_simp_tac Ssum_ss 1),
   23.67 +	(Asm_simp_tac 1),
   23.68  	(hyp_subst_tac 1),
   23.69 -	(asm_simp_tac Ssum_ss 1),
   23.70 +	(Asm_simp_tac 1),
   23.71  	(rtac monofun_cfun_arg 1),
   23.72  	(etac (less_ssum3b  RS iffD1) 1)
   23.73  	]);
   23.74 @@ -247,8 +247,8 @@
   23.75  	(cut_facts_tac prems 1),
   23.76  	(hyp_subst_tac 1),
   23.77  	(res_inst_tac [("Q","x=UU")] classical2 1),
   23.78 -	(asm_simp_tac Ssum_ss 1),
   23.79 -	(asm_simp_tac Ssum_ss 1)
   23.80 +	(Asm_simp_tac 1),
   23.81 +	(Asm_simp_tac 1)
   23.82  	]);
   23.83  
   23.84  (* ------------------------------------------------------------------------ *)
   23.85 @@ -262,8 +262,8 @@
   23.86  	(cut_facts_tac prems 1),
   23.87  	(hyp_subst_tac 1),
   23.88  	(res_inst_tac [("Q","x=UU")] classical2 1),
   23.89 -	(asm_simp_tac Ssum_ss 1),
   23.90 -	(asm_simp_tac Ssum_ss 1)
   23.91 +	(Asm_simp_tac 1),
   23.92 +	(Asm_simp_tac 1)
   23.93  	]);
   23.94  
   23.95  (* ------------------------------------------------------------------------ *)
   23.96 @@ -339,8 +339,8 @@
   23.97  	(rtac chain_UU_I_inverse 1),
   23.98  	(rtac allI 1),
   23.99  	(res_inst_tac [("p","Y(i)")] IssumE 1),
  23.100 -	(asm_simp_tac Ssum_ss 1),
  23.101 -	(asm_simp_tac Ssum_ss 2),
  23.102 +	(Asm_simp_tac 1),
  23.103 +	(Asm_simp_tac 2),
  23.104  	(etac notE 1),
  23.105  	(rtac (less_ssum3c RS iffD1) 1),
  23.106  	(res_inst_tac [("t","Isinl(x)")] subst 1),
  23.107 @@ -374,8 +374,8 @@
  23.108  	(rtac chain_UU_I_inverse 1),
  23.109  	(rtac allI 1),
  23.110  	(res_inst_tac [("p","Y(i)")] IssumE 1),
  23.111 -	(asm_simp_tac Ssum_ss 1),
  23.112 -	(asm_simp_tac Ssum_ss 1),
  23.113 +	(Asm_simp_tac 1),
  23.114 +	(Asm_simp_tac 1),
  23.115  	(etac notE 1),
  23.116  	(rtac (less_ssum3d RS iffD1) 1),
  23.117  	(res_inst_tac [("t","Isinr(y)")] subst 1),
    24.1 --- a/src/HOLCF/Ssum3.ML	Wed Oct 04 13:12:14 1995 +0100
    24.2 +++ b/src/HOLCF/Ssum3.ML	Wed Oct 04 14:01:44 1995 +0100
    24.3 @@ -41,8 +41,8 @@
    24.4  	(etac (monofun_Isinl RS ch2ch_monofun) 1),
    24.5  	(rtac allI 1),
    24.6  	(res_inst_tac [("Q","Y(k)=UU")] classical2 1),
    24.7 -	(asm_simp_tac Ssum_ss 1),
    24.8 -	(asm_simp_tac Ssum_ss 1)
    24.9 +	(Asm_simp_tac 1),
   24.10 +	(Asm_simp_tac 1)
   24.11  	]);
   24.12  
   24.13  qed_goal "contlub_Isinr" Ssum3.thy "contlub(Isinr)"
   24.14 @@ -72,8 +72,8 @@
   24.15  	(etac (monofun_Isinr RS ch2ch_monofun) 1),
   24.16  	(rtac allI 1),
   24.17  	(res_inst_tac [("Q","Y(k)=UU")] classical2 1),
   24.18 -	(asm_simp_tac Ssum_ss 1),
   24.19 -	(asm_simp_tac Ssum_ss 1)
   24.20 +	(Asm_simp_tac 1),
   24.21 +	(Asm_simp_tac 1)
   24.22  	]);
   24.23  
   24.24  qed_goal "cont_Isinl" Ssum3.thy "cont(Isinl)"
   24.25 @@ -114,11 +114,11 @@
   24.26  	(rtac (expand_fun_eq RS iffD2) 1),
   24.27  	(strip_tac 1),
   24.28  	(res_inst_tac [("p","xa")] IssumE 1),
   24.29 -	(asm_simp_tac Ssum_ss 1),
   24.30 +	(Asm_simp_tac 1),
   24.31  	(rtac (lub_const RS thelubI RS sym) 1),
   24.32 -	(asm_simp_tac Ssum_ss 1),
   24.33 +	(Asm_simp_tac 1),
   24.34  	(etac contlub_cfun_fun 1),
   24.35 -	(asm_simp_tac Ssum_ss 1),
   24.36 +	(Asm_simp_tac 1),
   24.37  	(rtac (lub_const RS thelubI RS sym) 1)
   24.38  	]);
   24.39  
   24.40 @@ -133,11 +133,11 @@
   24.41  	(rtac (expand_fun_eq RS iffD2) 1),
   24.42  	(strip_tac 1),
   24.43  	(res_inst_tac [("p","x")] IssumE 1),
   24.44 -	(asm_simp_tac Ssum_ss 1),
   24.45 +	(Asm_simp_tac 1),
   24.46  	(rtac (lub_const RS thelubI RS sym) 1),
   24.47 -	(asm_simp_tac Ssum_ss 1),
   24.48 +	(Asm_simp_tac 1),
   24.49  	(rtac (lub_const RS thelubI RS sym) 1),
   24.50 -	(asm_simp_tac Ssum_ss 1),
   24.51 +	(Asm_simp_tac 1),
   24.52  	(etac contlub_cfun_fun 1)
   24.53  	]);
   24.54  
   24.55 @@ -192,7 +192,7 @@
   24.56   (fn prems =>
   24.57  	[
   24.58  	(cut_facts_tac prems 1),
   24.59 -	(asm_simp_tac Ssum_ss 1),
   24.60 +	(Asm_simp_tac 1),
   24.61  	(rtac (chain_UU_I_inverse RS sym) 1),
   24.62  	(rtac allI 1),
   24.63  	(res_inst_tac [("s","Isinl(UU)"),("t","Y(i)")] subst 1),
   24.64 @@ -200,7 +200,7 @@
   24.65  	(rtac (chain_UU_I RS spec RS sym) 1),
   24.66  	(atac 1),
   24.67  	(etac (inst_ssum_pcpo RS ssubst) 1),
   24.68 -	(asm_simp_tac Ssum_ss 1)
   24.69 +	(Asm_simp_tac 1)
   24.70  	]);
   24.71  
   24.72  qed_goal "ssum_lemma12" Ssum3.thy 
   24.73 @@ -209,7 +209,7 @@
   24.74   (fn prems =>
   24.75  	[
   24.76  	(cut_facts_tac prems 1),
   24.77 -	(asm_simp_tac Ssum_ss 1),
   24.78 +	(Asm_simp_tac 1),
   24.79  	(res_inst_tac [("t","x")] subst 1),
   24.80  	(rtac inject_Isinl 1),
   24.81  	(rtac trans 1),
   24.82 @@ -255,7 +255,7 @@
   24.83  	(res_inst_tac [("t","Y(i)")] ssubst 1),
   24.84  	(atac 1),
   24.85  	(fast_tac HOL_cs 1),
   24.86 -	(simp_tac Cfun_ss 1),
   24.87 +	(Simp_tac 1),
   24.88  	(rtac (monofun_fapp2 RS ch2ch_monofun) 1),
   24.89  	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
   24.90  	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
   24.91 @@ -268,7 +268,7 @@
   24.92   (fn prems =>
   24.93  	[
   24.94  	(cut_facts_tac prems 1),
   24.95 -	(asm_simp_tac Ssum_ss 1),
   24.96 +	(Asm_simp_tac 1),
   24.97  	(res_inst_tac [("t","x")] subst 1),
   24.98  	(rtac inject_Isinr 1),
   24.99  	(rtac trans 1),
  24.100 @@ -319,7 +319,7 @@
  24.101  	(res_inst_tac [("t","Y(i)")] ssubst 1),
  24.102  	(atac 1),
  24.103  	(fast_tac HOL_cs 1),
  24.104 -	(simp_tac Cfun_ss 1),
  24.105 +	(Simp_tac 1),
  24.106  	(rtac (monofun_fapp2 RS ch2ch_monofun) 1),
  24.107  	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
  24.108  	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
  24.109 @@ -373,14 +373,14 @@
  24.110  qed_goalw "strict_sinl" Ssum3.thy [sinl_def] "sinl`UU =UU"
  24.111   (fn prems =>
  24.112  	[
  24.113 -	(simp_tac (Ssum_ss addsimps [cont_Isinl]) 1),
  24.114 +	(simp_tac (!simpset addsimps [cont_Isinl]) 1),
  24.115  	(rtac (inst_ssum_pcpo RS sym) 1)
  24.116  	]);
  24.117  
  24.118  qed_goalw "strict_sinr" Ssum3.thy [sinr_def] "sinr`UU=UU"
  24.119   (fn prems =>
  24.120  	[
  24.121 -	(simp_tac (Ssum_ss addsimps [cont_Isinr]) 1),
  24.122 +	(simp_tac (!simpset addsimps [cont_Isinr]) 1),
  24.123  	(rtac (inst_ssum_pcpo RS sym) 1)
  24.124  	]);
  24.125  
  24.126 @@ -391,8 +391,8 @@
  24.127  	(cut_facts_tac prems 1),
  24.128  	(rtac noteq_IsinlIsinr 1),
  24.129  	(etac box_equals 1),
  24.130 -	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1),
  24.131 -	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1)
  24.132 +	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
  24.133 +	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1)
  24.134  	]);
  24.135  
  24.136  qed_goalw "inject_sinl" Ssum3.thy [sinl_def,sinr_def] 
  24.137 @@ -402,8 +402,8 @@
  24.138  	(cut_facts_tac prems 1),
  24.139  	(rtac inject_Isinl 1),
  24.140  	(etac box_equals 1),
  24.141 -	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1),
  24.142 -	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1)
  24.143 +	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
  24.144 +	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1)
  24.145  	]);
  24.146  
  24.147  qed_goalw "inject_sinr" Ssum3.thy [sinl_def,sinr_def] 
  24.148 @@ -413,8 +413,8 @@
  24.149  	(cut_facts_tac prems 1),
  24.150  	(rtac inject_Isinr 1),
  24.151  	(etac box_equals 1),
  24.152 -	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1),
  24.153 -	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1)
  24.154 +	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
  24.155 +	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1)
  24.156  	]);
  24.157  
  24.158  
  24.159 @@ -444,7 +444,7 @@
  24.160  	"z=UU | (? a. z=sinl`a & a~=UU) | (? b. z=sinr`b & b~=UU)"
  24.161   (fn prems =>
  24.162  	[
  24.163 -	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1),
  24.164 +	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
  24.165  	(rtac (inst_ssum_pcpo RS ssubst) 1),
  24.166  	(rtac Exh_Ssum 1)
  24.167  	]);
  24.168 @@ -462,10 +462,10 @@
  24.169  	(atac 1),
  24.170  	(resolve_tac prems 1),
  24.171  	(atac 2),
  24.172 -	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1),
  24.173 +	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
  24.174  	(resolve_tac prems 1),
  24.175  	(atac 2),
  24.176 -	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1)
  24.177 +	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1)
  24.178  	]);
  24.179  
  24.180  
  24.181 @@ -499,7 +499,7 @@
  24.182  	(rtac (beta_cfun RS ssubst) 1),
  24.183  	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  24.184  		cont_Iwhen3,cont2cont_CF1L]) 1)),
  24.185 -	(simp_tac Ssum_ss  1)
  24.186 +	(Simp_tac 1)
  24.187  	]);
  24.188  
  24.189  qed_goalw "sswhen2" Ssum3.thy [sswhen_def,sinl_def,sinr_def] 
  24.190 @@ -519,7 +519,7 @@
  24.191  	(rtac (beta_cfun RS ssubst) 1),
  24.192  	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  24.193  		cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  24.194 -	(asm_simp_tac Ssum_ss  1)
  24.195 +	(Asm_simp_tac  1)
  24.196  	]);
  24.197  
  24.198  
  24.199 @@ -541,7 +541,7 @@
  24.200  	(rtac (beta_cfun RS ssubst) 1),
  24.201  	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  24.202  		cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  24.203 -	(asm_simp_tac Ssum_ss  1)
  24.204 +	(Asm_simp_tac 1)
  24.205  	]);
  24.206  
  24.207  
  24.208 @@ -602,7 +602,7 @@
  24.209   (fn prems =>
  24.210  	[
  24.211  	(cut_facts_tac prems 1),
  24.212 -	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1),
  24.213 +	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
  24.214  	(etac ssum_lemma4 1)
  24.215  	]);
  24.216  
  24.217 @@ -629,7 +629,7 @@
  24.218  	(rtac exI 1),
  24.219  	(etac box_equals 1),
  24.220  	(rtac refl 1),
  24.221 -	(asm_simp_tac (Ssum_ss addsimps [cont_Isinl]) 1)
  24.222 +	(asm_simp_tac (!simpset addsimps [cont_Isinl]) 1)
  24.223  	]);
  24.224  
  24.225  qed_goalw "thelub_ssum2b" Ssum3.thy [sinl_def,sinr_def,sswhen_def] 
  24.226 @@ -658,7 +658,7 @@
  24.227  	(rtac exI 1),
  24.228  	(etac box_equals 1),
  24.229  	(rtac refl 1),
  24.230 -	(asm_simp_tac (Ssum_ss addsimps 
  24.231 +	(asm_simp_tac (!simpset addsimps 
  24.232  	[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
  24.233  	cont_Iwhen3]) 1)
  24.234  	]);
  24.235 @@ -668,11 +668,11 @@
  24.236   (fn prems =>
  24.237  	[
  24.238  	(cut_facts_tac prems 1),
  24.239 -	(asm_simp_tac (Ssum_ss addsimps 
  24.240 +	(asm_simp_tac (!simpset addsimps 
  24.241  	[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
  24.242  	cont_Iwhen3]) 1),
  24.243  	(etac ssum_lemma9 1),
  24.244 -	(asm_simp_tac (Ssum_ss addsimps 
  24.245 +	(asm_simp_tac (!simpset addsimps 
  24.246  	[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
  24.247  	cont_Iwhen3]) 1)
  24.248  	]);
  24.249 @@ -682,11 +682,11 @@
  24.250   (fn prems =>
  24.251  	[
  24.252  	(cut_facts_tac prems 1),
  24.253 -	(asm_simp_tac (Ssum_ss addsimps 
  24.254 +	(asm_simp_tac (!simpset addsimps 
  24.255  	[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
  24.256  	cont_Iwhen3]) 1),
  24.257  	(etac ssum_lemma10 1),
  24.258 -	(asm_simp_tac (Ssum_ss addsimps 
  24.259 +	(asm_simp_tac (!simpset addsimps 
  24.260  	[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
  24.261  	cont_Iwhen3]) 1)
  24.262  	]);
  24.263 @@ -714,9 +714,9 @@
  24.264   (fn prems =>
  24.265  	[
  24.266  	(res_inst_tac [("p","z")] ssumE 1),
  24.267 -	(asm_simp_tac (Cfun_ss addsimps [sswhen1,sswhen2,sswhen3]) 1),
  24.268 -	(asm_simp_tac (Cfun_ss addsimps [sswhen1,sswhen2,sswhen3]) 1),
  24.269 -	(asm_simp_tac (Cfun_ss addsimps [sswhen1,sswhen2,sswhen3]) 1)
  24.270 +	(asm_simp_tac (!simpset addsimps [sswhen1,sswhen2,sswhen3]) 1),
  24.271 +	(asm_simp_tac (!simpset addsimps [sswhen1,sswhen2,sswhen3]) 1),
  24.272 +	(asm_simp_tac (!simpset addsimps [sswhen1,sswhen2,sswhen3]) 1)
  24.273  	]);
  24.274  
  24.275  
  24.276 @@ -724,5 +724,4 @@
  24.277  (* install simplifier for Ssum                                              *)
  24.278  (* ------------------------------------------------------------------------ *)
  24.279  
  24.280 -val Ssum_rews = [strict_sinl,strict_sinr,sswhen1,sswhen2,sswhen3];
  24.281 -val Ssum_ss = Cfun_ss addsimps Ssum_rews;
  24.282 +Addsimps [strict_sinl,strict_sinr,sswhen1,sswhen2,sswhen3];
    25.1 --- a/src/HOLCF/Stream.ML	Wed Oct 04 13:12:14 1995 +0100
    25.2 +++ b/src/HOLCF/Stream.ML	Wed Oct 04 14:01:44 1995 +0100
    25.3 @@ -26,7 +26,7 @@
    25.4   (fn prems =>
    25.5  	[
    25.6  	(cut_facts_tac prems 1),
    25.7 -	(asm_simp_tac (HOLCF_ss addsimps 
    25.8 +	(asm_simp_tac (!simpset addsimps 
    25.9  		(stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
   25.10  	]);
   25.11  
   25.12 @@ -47,18 +47,18 @@
   25.13  	"s = UU | (? x xs. x~=UU & s = scons`x`xs)"
   25.14   (fn prems =>
   25.15  	[
   25.16 -	(simp_tac HOLCF_ss  1),
   25.17 +	(Simp_tac 1),
   25.18  	(rtac (stream_rep_iso RS subst) 1),
   25.19  	(res_inst_tac [("p","stream_rep`s")] sprodE 1),
   25.20 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   25.21 -	(asm_simp_tac HOLCF_ss  1),
   25.22 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
   25.23 +	(Asm_simp_tac  1),
   25.24  	(res_inst_tac [("p","y")] liftE1 1),
   25.25  	(contr_tac 1),
   25.26  	(rtac disjI2 1),
   25.27  	(rtac exI 1),
   25.28  	(rtac exI 1),
   25.29  	(etac conjI 1),
   25.30 -	(asm_simp_tac HOLCF_ss  1)
   25.31 +	(Asm_simp_tac  1)
   25.32  	]);
   25.33  
   25.34  qed_goal "streamE" Stream.thy 
   25.35 @@ -82,7 +82,7 @@
   25.36   (fn prems =>
   25.37  	[
   25.38  	(cut_facts_tac prems 1),
   25.39 -	(asm_simp_tac (HOLCF_ss addsimps 
   25.40 +	(asm_simp_tac (!simpset addsimps 
   25.41  		(stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
   25.42  	]);
   25.43  
   25.44 @@ -102,7 +102,7 @@
   25.45  fun prover defs thm = prove_goalw Stream.thy defs thm
   25.46   (fn prems =>
   25.47  	[
   25.48 -	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
   25.49 +	(simp_tac (!simpset addsimps stream_rews) 1)
   25.50  	]);
   25.51  
   25.52  val stream_discsel = [
   25.53 @@ -115,7 +115,7 @@
   25.54   (fn prems =>
   25.55  	[
   25.56  	(cut_facts_tac prems 1),
   25.57 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   25.58 +	(asm_simp_tac (!simpset addsimps stream_rews) 1)
   25.59  	]);
   25.60  
   25.61  val stream_discsel = [
   25.62 @@ -134,10 +134,10 @@
   25.63   (fn prems =>
   25.64  	[
   25.65  	(res_inst_tac [("P1",contr)] classical3 1),
   25.66 -	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   25.67 +	(simp_tac (!simpset addsimps stream_rews) 1),
   25.68  	(dtac sym 1),
   25.69 -	(asm_simp_tac HOLCF_ss  1),
   25.70 -	(simp_tac (HOLCF_ss addsimps (prems @ stream_rews)) 1)
   25.71 +	(Asm_simp_tac 1),
   25.72 +	(simp_tac (!simpset addsimps (prems @ stream_rews)) 1)
   25.73  	]);
   25.74  
   25.75  val stream_constrdef = [
   25.76 @@ -147,7 +147,7 @@
   25.77  fun prover defs thm = prove_goalw Stream.thy defs thm
   25.78   (fn prems =>
   25.79  	[
   25.80 -	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
   25.81 +	(simp_tac (!simpset addsimps stream_rews) 1)
   25.82  	]);
   25.83  
   25.84  val stream_constrdef = [
   25.85 @@ -176,12 +176,12 @@
   25.86  	(rtac conjI 1),
   25.87  	(dres_inst_tac [("fo5","stream_when`(LAM x l.x)")] monofun_cfun_arg 1),
   25.88  	(etac box_less 1),
   25.89 -	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
   25.90 -	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
   25.91 +	(asm_simp_tac (!simpset addsimps stream_when) 1),
   25.92 +	(asm_simp_tac (!simpset addsimps stream_when) 1),
   25.93  	(dres_inst_tac [("fo5","stream_when`(LAM x l.l)")] monofun_cfun_arg 1),
   25.94  	(etac box_less 1),
   25.95 -	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
   25.96 -	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1)
   25.97 +	(asm_simp_tac (!simpset addsimps stream_when) 1),
   25.98 +	(asm_simp_tac (!simpset addsimps stream_when) 1)
   25.99  	])
  25.100  	];
  25.101  
  25.102 @@ -199,12 +199,12 @@
  25.103  	(rtac conjI 1),
  25.104  	(dres_inst_tac [("f","stream_when`(LAM x l.x)")] cfun_arg_cong 1),
  25.105  	(etac box_equals 1),
  25.106 -	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
  25.107 -	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
  25.108 +	(asm_simp_tac (!simpset addsimps stream_when) 1),
  25.109 +	(asm_simp_tac (!simpset addsimps stream_when) 1),
  25.110  	(dres_inst_tac [("f","stream_when`(LAM x l.l)")] cfun_arg_cong 1),
  25.111  	(etac box_equals 1),
  25.112 -	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
  25.113 -	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1)
  25.114 +	(asm_simp_tac (!simpset addsimps stream_when) 1),
  25.115 +	(asm_simp_tac (!simpset addsimps stream_when) 1)
  25.116  	])
  25.117  	];
  25.118  
  25.119 @@ -218,7 +218,7 @@
  25.120  	(cut_facts_tac prems 1),
  25.121  	(rtac streamE 1),
  25.122  	(contr_tac 1),
  25.123 -	(REPEAT (asm_simp_tac (HOLCF_ss addsimps stream_discsel) 1))
  25.124 +	(REPEAT (asm_simp_tac (!simpset addsimps stream_discsel) 1))
  25.125  	]);
  25.126  
  25.127  val stream_discsel_def = 
  25.128 @@ -240,22 +240,22 @@
  25.129   (fn prems =>
  25.130  	[
  25.131  	(res_inst_tac [("n","n")] natE 1),
  25.132 -	(asm_simp_tac iterate_ss 1),
  25.133 -	(asm_simp_tac iterate_ss 1),
  25.134 -	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
  25.135 +	(Asm_simp_tac 1),
  25.136 +	(Asm_simp_tac 1),
  25.137 +	(simp_tac (!simpset addsimps stream_rews) 1)
  25.138  	]),
  25.139  prove_goalw Stream.thy [stream_take_def] "stream_take 0`xs=UU"
  25.140   (fn prems =>
  25.141  	[
  25.142 -	(asm_simp_tac iterate_ss 1)
  25.143 +	(Asm_simp_tac 1)
  25.144  	])];
  25.145  
  25.146  fun prover thm = prove_goalw Stream.thy [stream_take_def] thm
  25.147   (fn prems =>
  25.148  	[
  25.149  	(cut_facts_tac prems 1),
  25.150 -	(simp_tac iterate_ss 1),
  25.151 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
  25.152 +	(Simp_tac 1),
  25.153 +	(asm_simp_tac (!simpset addsimps stream_rews) 1)
  25.154  	]);
  25.155  
  25.156  val stream_take = [
  25.157 @@ -274,16 +274,16 @@
  25.158   (fn prems =>
  25.159  	[
  25.160  	(res_inst_tac [("Q","x=UU")] classical2 1),
  25.161 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.162 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
  25.163 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
  25.164 +	(asm_simp_tac (!simpset addsimps stream_rews) 1)
  25.165  	]);
  25.166  
  25.167  qed_goal "shd2" Stream.thy "shd`(scons`x`xs) = x"
  25.168   (fn prems =>
  25.169  	[
  25.170  	(res_inst_tac [("Q","x=UU")] classical2 1),
  25.171 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.172 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
  25.173 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
  25.174 +	(asm_simp_tac (!simpset addsimps stream_rews) 1)
  25.175  	]);
  25.176  
  25.177  qed_goal "stream_take2" Stream.thy 
  25.178 @@ -291,8 +291,8 @@
  25.179   (fn prems =>
  25.180  	[
  25.181  	(res_inst_tac [("Q","x=UU")] classical2 1),
  25.182 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.183 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
  25.184 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
  25.185 +	(asm_simp_tac (!simpset addsimps stream_rews) 1)
  25.186  	]);
  25.187  
  25.188  val stream_rews = [stream_iso_strict RS conjunct1,
  25.189 @@ -351,15 +351,15 @@
  25.190  	[
  25.191  	(cut_facts_tac prems 1),
  25.192  	(nat_ind_tac "n" 1),
  25.193 -	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.194 +	(simp_tac (!simpset addsimps stream_rews) 1),
  25.195  	(strip_tac 1),
  25.196  	((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
  25.197  	(atac 1),
  25.198 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.199 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
  25.200  	(etac exE 1),
  25.201  	(etac exE 1),
  25.202  	(etac exE 1),
  25.203 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.204 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
  25.205  	(REPEAT (etac conjE 1)),
  25.206  	(rtac cfun_arg_cong 1),
  25.207  	(fast_tac HOL_cs 1)
  25.208 @@ -385,13 +385,13 @@
  25.209   (fn prems =>
  25.210  	[
  25.211  	(nat_ind_tac "n" 1),
  25.212 -	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.213 +	(simp_tac (!simpset addsimps stream_rews) 1),
  25.214  	(resolve_tac prems 1),
  25.215  	(rtac allI 1),
  25.216  	(res_inst_tac [("s","s")] streamE 1),
  25.217 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.218 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
  25.219  	(resolve_tac prems 1),
  25.220 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.221 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
  25.222  	(resolve_tac prems 1),
  25.223  	(atac 1),
  25.224  	(etac spec 1)
  25.225 @@ -473,8 +473,8 @@
  25.226   (fn prems =>
  25.227  	[
  25.228  	(res_inst_tac [("s","s")] streamE 1),
  25.229 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.230 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
  25.231 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
  25.232 +	(asm_simp_tac (!simpset addsimps stream_rews) 1)
  25.233  	]);
  25.234  
  25.235  
  25.236 @@ -500,18 +500,18 @@
  25.237  	(res_inst_tac [("x","stl`s2")] exI 1),
  25.238  	(rtac conjI 1),
  25.239  	(eresolve_tac stream_discsel_def 1),
  25.240 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
  25.241 +	(asm_simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1),
  25.242  	(eres_inst_tac [("s","shd`s1"),("t","shd`s2")] subst 1),
  25.243 -	(simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
  25.244 +	(simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1),
  25.245  	(res_inst_tac [("x","shd`s2")] exI 1),
  25.246  	(res_inst_tac [("x","stl`s1")] exI 1),
  25.247  	(res_inst_tac [("x","stl`s2")] exI 1),
  25.248  	(rtac conjI 1),
  25.249  	(eresolve_tac stream_discsel_def 1),
  25.250 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
  25.251 +	(asm_simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1),
  25.252  	(res_inst_tac [("s","shd`s1"),("t","shd`s2")] ssubst 1),
  25.253  	(etac sym 1),
  25.254 -	(simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1)
  25.255 +	(simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1)
  25.256  	]);
  25.257  
  25.258  
  25.259 @@ -528,7 +528,7 @@
  25.260   (fn prems =>
  25.261  	[
  25.262  	(rtac exI 1),
  25.263 -	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
  25.264 +	(simp_tac (!simpset addsimps stream_rews) 1)
  25.265  	]);
  25.266  
  25.267  qed_goal "inf_stream_not_UU" Stream.thy  "~stream_finite(s)  ==> s ~= UU"
  25.268 @@ -549,9 +549,9 @@
  25.269   (fn prems =>
  25.270  	[
  25.271  	(res_inst_tac [("s","s")] streamE 1),
  25.272 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.273 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
  25.274  	(hyp_subst_tac 1),
  25.275 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
  25.276 +	(asm_simp_tac (!simpset addsimps stream_rews) 1)
  25.277  	]);
  25.278  
  25.279  
  25.280 @@ -567,7 +567,7 @@
  25.281  	(rtac allI 1),
  25.282  	(rtac allI 1),
  25.283  	(rtac impI 1),
  25.284 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.285 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
  25.286  	(strip_tac 1),
  25.287  	(rtac ((hd stream_inject) RS conjunct2) 1),
  25.288  	(atac 1),
  25.289 @@ -581,14 +581,14 @@
  25.290   (fn prems =>
  25.291  	[
  25.292  	(nat_ind_tac "n" 1),
  25.293 -	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.294 +	(simp_tac (!simpset addsimps stream_rews) 1),
  25.295  	(strip_tac 1 ),
  25.296  	(hyp_subst_tac  1),
  25.297 -	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.298 +	(simp_tac (!simpset addsimps stream_rews) 1),
  25.299  	(rtac allI 1),
  25.300  	(res_inst_tac [("s","s2")] streamE 1),
  25.301 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.302 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.303 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
  25.304 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
  25.305  	(strip_tac 1 ),
  25.306  	(subgoal_tac "stream_take n1`xs = xs" 1),
  25.307  	(rtac ((hd stream_inject) RS conjunct2) 2),
  25.308 @@ -605,7 +605,7 @@
  25.309   (fn prems =>
  25.310  	[
  25.311  	(nat_ind_tac "n" 1),
  25.312 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.313 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
  25.314  	(strip_tac 1 ),
  25.315  	(res_inst_tac [("P","scons`x`xs=UU")] notE 1),
  25.316  	(eresolve_tac stream_constrdef 1),
  25.317 @@ -624,8 +624,8 @@
  25.318   (fn prems =>
  25.319  	[
  25.320  	(nat_ind_tac "n" 1),
  25.321 -	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.322 -	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
  25.323 +	(simp_tac (!simpset addsimps stream_rews) 1),
  25.324 +	(simp_tac (!simpset addsimps stream_rews) 1)
  25.325  	]);
  25.326  
  25.327  (* ---- *)
  25.328 @@ -635,15 +635,15 @@
  25.329   (fn prems =>
  25.330  	[
  25.331  	(nat_ind_tac "n" 1),
  25.332 -	(simp_tac iterate_ss 1),
  25.333 -	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.334 +	(Simp_tac 1),
  25.335 +	(simp_tac (!simpset addsimps stream_rews) 1),
  25.336  	(strip_tac 1),
  25.337  	(res_inst_tac [("s","s")] streamE 1),
  25.338  	(hyp_subst_tac 1),
  25.339  	(rtac (iterate_Suc2 RS ssubst) 1),
  25.340 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.341 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
  25.342  	(rtac (iterate_Suc2 RS ssubst) 1),
  25.343 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.344 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
  25.345  	(etac allE 1),
  25.346  	(etac mp 1),
  25.347  	(hyp_subst_tac 1),
  25.348 @@ -656,16 +656,16 @@
  25.349   (fn prems =>
  25.350  	[
  25.351  	(nat_ind_tac "n" 1),
  25.352 -	(simp_tac iterate_ss 1),
  25.353 +	(Simp_tac 1),
  25.354  	(strip_tac 1),
  25.355 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.356 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
  25.357  	(rtac allI 1),
  25.358  	(res_inst_tac [("s","s")] streamE 1),
  25.359  	(hyp_subst_tac 1),
  25.360 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.361 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
  25.362  	(hyp_subst_tac 1),
  25.363  	(rtac (iterate_Suc2 RS ssubst) 1),
  25.364 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
  25.365 +	(asm_simp_tac (!simpset addsimps stream_rews) 1)
  25.366  	]);
  25.367  
  25.368  qed_goal "stream_take_lemma7" Stream.thy 
  25.369 @@ -744,7 +744,7 @@
  25.370   (fn prems =>
  25.371  	[
  25.372  	(nat_ind_tac "n" 1),
  25.373 -	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.374 +	(simp_tac (!simpset addsimps stream_rews) 1),
  25.375  	(strip_tac 1 ),
  25.376  	(hyp_subst_tac  1),
  25.377  	(dtac UU_I 1),
  25.378 @@ -761,9 +761,9 @@
  25.379  	(hyp_subst_tac  1),
  25.380  	(strip_tac 1 ),
  25.381  	(dtac UU_I 1),
  25.382 -	(asm_simp_tac(HOLCF_ss addsimps (stream_rews @ [stream_finite_UU])) 1),
  25.383 +	(asm_simp_tac(!simpset addsimps (stream_rews @ [stream_finite_UU])) 1),
  25.384  	(hyp_subst_tac  1),
  25.385 -	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
  25.386 +	(simp_tac (!simpset addsimps stream_rews) 1),
  25.387  	(strip_tac 1 ),
  25.388  	(rtac stream_finite_lemma1 1),
  25.389  	(subgoal_tac "xs << xsa" 1),
  25.390 @@ -794,7 +794,7 @@
  25.391  "stream_finite(s) = (? n. iterate n stl s = UU)"
  25.392   (fn prems =>
  25.393  	[
  25.394 -	(simp_tac (HOL_ss addsimps [stream_take_lemma7]) 1)
  25.395 +	(simp_tac (!simpset addsimps [stream_take_lemma7]) 1)
  25.396  	]);
  25.397  
  25.398  
    26.1 --- a/src/HOLCF/Stream2.ML	Wed Oct 04 13:12:14 1995 +0100
    26.2 +++ b/src/HOLCF/Stream2.ML	Wed Oct 04 14:01:44 1995 +0100
    26.3 @@ -25,7 +25,7 @@
    26.4   (fn prems =>
    26.5  	[
    26.6  	(rtac (smap_def2 RS ssubst) 1),
    26.7 -	(simp_tac (HOLCF_ss addsimps stream_when) 1)
    26.8 +	(simp_tac (!simpset addsimps stream_when) 1)
    26.9  	]);
   26.10  
   26.11  qed_goal "smap2" Stream2.thy 
   26.12 @@ -35,7 +35,7 @@
   26.13  	(cut_facts_tac prems 1),
   26.14  	(rtac trans 1),
   26.15  	(rtac (smap_def2 RS ssubst) 1),
   26.16 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   26.17 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
   26.18  	(rtac refl 1)
   26.19  	]);
   26.20  
    27.1 --- a/src/HOLCF/Tr1.ML	Wed Oct 04 13:12:14 1995 +0100
    27.2 +++ b/src/HOLCF/Tr1.ML	Wed Oct 04 14:01:44 1995 +0100
    27.3 @@ -129,15 +129,15 @@
    27.4  	(rtac allI 1),
    27.5  	(rtac allI 1),
    27.6  	(res_inst_tac [("p","x")] trE 1),
    27.7 -	(asm_simp_tac ccc1_ss 1),
    27.8 +	(Asm_simp_tac 1),
    27.9  	(res_inst_tac [("p","y")] trE 1),
   27.10 -	(asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1),
   27.11 -	(asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1),
   27.12 -	(asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1),
   27.13 +	(asm_simp_tac (!simpset addsimps dist_less_tr) 1),
   27.14 +	(asm_simp_tac (!simpset addsimps dist_less_tr) 1),
   27.15 +	(asm_simp_tac (!simpset addsimps dist_less_tr) 1),
   27.16  	(res_inst_tac [("p","y")] trE 1),
   27.17 -	(asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1),
   27.18 -	(asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1),
   27.19 -	(asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1)
   27.20 +	(asm_simp_tac (!simpset addsimps dist_less_tr) 1),
   27.21 +	(asm_simp_tac (!simpset addsimps dist_less_tr) 1),
   27.22 +	(asm_simp_tac (!simpset addsimps dist_less_tr) 1)
   27.23  	]);
   27.24  
   27.25  
   27.26 @@ -148,8 +148,8 @@
   27.27  fun prover s =  prove_goalw Tr1.thy [tr_when_def,TT_def,FF_def] s
   27.28   (fn prems =>
   27.29  	[
   27.30 -	(simp_tac Cfun_ss 1),
   27.31 -	(simp_tac (Ssum_ss addsimps [(rep_tr_iso ),
   27.32 +	(Simp_tac 1),
   27.33 +	(simp_tac (!simpset addsimps [(rep_tr_iso ),
   27.34  		(abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) 
   27.35  		RS iso_strict) RS conjunct1]@dist_eq_one)1)
   27.36  	]);
    28.1 --- a/src/HOLCF/Tr2.ML	Wed Oct 04 13:12:14 1995 +0100
    28.2 +++ b/src/HOLCF/Tr2.ML	Wed Oct 04 14:01:44 1995 +0100
    28.3 @@ -15,7 +15,7 @@
    28.4  fun prover s =  prove_goalw Tr2.thy [andalso_def] s
    28.5   (fn prems =>
    28.6  	[
    28.7 -	(simp_tac (ccc1_ss addsimps tr_when) 1)
    28.8 +	(simp_tac (!simpset addsimps tr_when) 1)
    28.9  	]);
   28.10  
   28.11  val andalso_thms = map prover [
   28.12 @@ -29,9 +29,9 @@
   28.13   (fn prems =>
   28.14  	[
   28.15  	(res_inst_tac [("p","x")] trE 1),
   28.16 -	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
   28.17 -	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
   28.18 -	(asm_simp_tac (ccc1_ss addsimps tr_when) 1)
   28.19 +	(asm_simp_tac (!simpset addsimps tr_when) 1),
   28.20 +	(asm_simp_tac (!simpset addsimps tr_when) 1),
   28.21 +	(asm_simp_tac (!simpset addsimps tr_when) 1)
   28.22  	])];
   28.23  
   28.24  (* ------------------------------------------------------------------------ *) 
   28.25 @@ -41,7 +41,7 @@
   28.26  fun prover s =  prove_goalw Tr2.thy [orelse_def] s
   28.27   (fn prems =>
   28.28  	[
   28.29 -	(simp_tac (ccc1_ss addsimps tr_when) 1)
   28.30 +	(simp_tac (!simpset addsimps tr_when) 1)
   28.31  	]);
   28.32  
   28.33  val orelse_thms = map prover [
   28.34 @@ -55,9 +55,9 @@
   28.35   (fn prems =>
   28.36  	[
   28.37  	(res_inst_tac [("p","x")] trE 1),
   28.38 -	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
   28.39 -	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
   28.40 -	(asm_simp_tac (ccc1_ss addsimps tr_when) 1)
   28.41 +	(asm_simp_tac (!simpset addsimps tr_when) 1),
   28.42 +	(asm_simp_tac (!simpset addsimps tr_when) 1),
   28.43 +	(asm_simp_tac (!simpset addsimps tr_when) 1)
   28.44  	])];
   28.45  
   28.46  
   28.47 @@ -68,7 +68,7 @@
   28.48  fun prover s =  prove_goalw Tr2.thy [neg_def] s
   28.49   (fn prems =>
   28.50  	[
   28.51 -	(simp_tac (ccc1_ss addsimps tr_when) 1)
   28.52 +	(simp_tac (!simpset addsimps tr_when) 1)
   28.53  	]);
   28.54  
   28.55  val neg_thms = map prover [
   28.56 @@ -84,7 +84,7 @@
   28.57  fun prover s =  prove_goalw Tr2.thy [ifte_def] s
   28.58   (fn prems =>
   28.59  	[
   28.60 -	(simp_tac (ccc1_ss addsimps tr_when) 1)
   28.61 +	(simp_tac (!simpset addsimps tr_when) 1)
   28.62  	]);
   28.63  
   28.64  val ifte_thms = map prover [
    29.1 --- a/src/HOLCF/ccc1.ML	Wed Oct 04 13:12:14 1995 +0100
    29.2 +++ b/src/HOLCF/ccc1.ML	Wed Oct 04 14:01:44 1995 +0100
    29.3 @@ -87,8 +87,7 @@
    29.4  (* Merge the different rewrite rules for the simplifier                     *)
    29.5  (* ------------------------------------------------------------------------ *)
    29.6  
    29.7 -val ccc1_ss = Cfun_ss addsimps Cprod_rews addsimps Sprod_rews addsimps
    29.8 -		 Ssum_rews addsimps lift_rews addsimps [ID1,ID2,ID3,cfcomp2];
    29.9 +Addsimps (lift_rews @ [ID1,ID2,ID3,cfcomp2]);
   29.10  
   29.11  
   29.12  
    30.1 --- a/src/HOLCF/ex/Coind.ML	Wed Oct 04 13:12:14 1995 +0100
    30.2 +++ b/src/HOLCF/ex/Coind.ML	Wed Oct 04 14:01:44 1995 +0100
    30.3 @@ -29,7 +29,7 @@
    30.4  	[
    30.5  	(rtac trans 1),
    30.6  	(rtac (from_def2 RS ssubst) 1),
    30.7 -	(simp_tac HOLCF_ss  1),
    30.8 +	(Simp_tac 1),
    30.9  	(rtac refl 1)
   30.10  	]);
   30.11  
   30.12 @@ -58,19 +58,19 @@
   30.13   (fn prems =>
   30.14  	[
   30.15  	(res_inst_tac [("s","n")] dnat_ind 1),
   30.16 -	(simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
   30.17 -	(simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
   30.18 +	(simp_tac (!simpset addsimps (coind_rews @ stream_rews)) 1),
   30.19 +	(simp_tac (!simpset addsimps (coind_rews @ stream_rews)) 1),
   30.20  	(rtac trans 1),
   30.21  	(rtac nats_def2 1),
   30.22 -	(simp_tac (HOLCF_ss addsimps (coind_rews @ dnat_rews)) 1),
   30.23 +	(simp_tac (!simpset addsimps (coind_rews @ dnat_rews)) 1),
   30.24  	(rtac trans 1),
   30.25  	(etac iterator3 1),
   30.26  	(rtac trans 1),
   30.27 -	(asm_simp_tac HOLCF_ss 1),
   30.28 +	(Asm_simp_tac 1),
   30.29  	(rtac trans 1),
   30.30  	(etac smap2 1),
   30.31  	(rtac cfun_arg_cong 1),
   30.32 -	(asm_simp_tac (HOLCF_ss addsimps ([iterator3 RS sym] @ dnat_rews)) 1)
   30.33 +	(asm_simp_tac (!simpset addsimps ([iterator3 RS sym] @ dnat_rews)) 1)
   30.34  	]);
   30.35  
   30.36  
   30.37 @@ -80,13 +80,13 @@
   30.38  	(res_inst_tac [("R",
   30.39  "% p q.? n. p = iterator`n`(smap`dsucc)`nats & q = from`n")] stream_coind 1),
   30.40  	(res_inst_tac [("x","dzero")] exI 2),
   30.41 -	(asm_simp_tac (HOLCF_ss addsimps coind_rews) 2),
   30.42 +	(asm_simp_tac (!simpset addsimps coind_rews) 2),
   30.43  	(rewrite_goals_tac [stream_bisim_def]),
   30.44  	(strip_tac 1),
   30.45  	(etac exE 1),
   30.46  	(res_inst_tac [("Q","n=UU")] classical2 1),
   30.47  	(rtac disjI1 1),
   30.48 -	(asm_simp_tac (HOLCF_ss addsimps coind_rews) 1),
   30.49 +	(asm_simp_tac (!simpset addsimps coind_rews) 1),
   30.50  	(rtac disjI2 1),
   30.51  	(etac conjE 1),
   30.52  	(hyp_subst_tac 1),
   30.53 @@ -113,26 +113,26 @@
   30.54  	(strip_tac 1),
   30.55  	(etac exE 1),
   30.56  	(res_inst_tac [("Q","n=UU")] classical2 1),
   30.57 -	(asm_simp_tac (HOLCF_ss addsimps coind_rews) 1),
   30.58 +	(asm_simp_tac (!simpset addsimps coind_rews) 1),
   30.59  	(res_inst_tac [("x","UU::dnat")] exI 1),
   30.60 -	(simp_tac (HOLCF_ss addsimps coind_rews addsimps stream_rews) 1),
   30.61 +	(simp_tac (!simpset addsimps coind_rews addsimps stream_rews) 1),
   30.62  	(etac conjE 1),
   30.63  	(hyp_subst_tac 1),
   30.64  	(rtac conjI 1),
   30.65  	(rtac (coind_lemma1 RS ssubst) 1),
   30.66  	(rtac (from RS ssubst) 1),
   30.67 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   30.68 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
   30.69  	(res_inst_tac [("x","dsucc`n")] exI 1),
   30.70  	(rtac conjI 1),
   30.71  	(rtac trans 1),
   30.72  	(rtac (coind_lemma1 RS ssubst) 1),
   30.73 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   30.74 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
   30.75  	(rtac refl 1),
   30.76  	(rtac trans 1),
   30.77  	(rtac (from RS ssubst) 1),
   30.78 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   30.79 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
   30.80  	(rtac refl 1),
   30.81  	(res_inst_tac [("x","dzero")] exI 1),
   30.82 -	(asm_simp_tac (HOLCF_ss addsimps coind_rews) 1)
   30.83 +	(asm_simp_tac (!simpset addsimps coind_rews) 1)
   30.84  	]);
   30.85  
    31.1 --- a/src/HOLCF/ex/Dagstuhl.ML	Wed Oct 04 13:12:14 1995 +0100
    31.2 +++ b/src/HOLCF/ex/Dagstuhl.ML	Wed Oct 04 14:01:44 1995 +0100
    31.3 @@ -37,10 +37,10 @@
    31.4  val prems = goal Dagstuhl.thy "YS = YYS";
    31.5  by (rtac stream_take_lemma 1);
    31.6  by (nat_ind_tac "n" 1);
    31.7 -by (simp_tac (HOLCF_ss addsimps stream_rews) 1);
    31.8 +by (simp_tac (!simpset addsimps stream_rews) 1);
    31.9  by (rtac (YS_def2 RS ssubst) 1);
   31.10  by (rtac (YYS_def2 RS ssubst) 1);
   31.11 -by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
   31.12 +by (asm_simp_tac (!simpset addsimps stream_rews) 1);
   31.13  by (rtac (lemma5 RS sym RS subst) 1);
   31.14  by (rtac refl 1);
   31.15  val wir_moel=result();
   31.16 @@ -56,7 +56,7 @@
   31.17  by (rtac fix_least 1);
   31.18  by (rtac (beta_cfun RS ssubst) 1);
   31.19  by (cont_tacR 1);
   31.20 -by (simp_tac (HOLCF_ss addsimps [YS_def2 RS sym]) 1);
   31.21 +by (simp_tac (!simpset addsimps [YS_def2 RS sym]) 1);
   31.22  val lemma6=result();
   31.23  
   31.24  val prems = goal Dagstuhl.thy "YS << YYS";
    32.1 --- a/src/HOLCF/ex/Hoare.ML	Wed Oct 04 13:12:14 1995 +0100
    32.2 +++ b/src/HOLCF/ex/Hoare.ML	Wed Oct 04 14:01:44 1995 +0100
    32.3 @@ -124,7 +124,7 @@
    32.4   (fn prems =>
    32.5  	[
    32.6  	(fix_tac3 p_def 1),
    32.7 -	(simp_tac HOLCF_ss 1)
    32.8 +	(Simp_tac 1)
    32.9  	]);
   32.10  
   32.11  val q_def3 = prove_goal Hoare.thy 
   32.12 @@ -132,19 +132,21 @@
   32.13   (fn prems =>
   32.14  	[
   32.15  	(fix_tac3 q_def 1),
   32.16 -	(simp_tac HOLCF_ss 1)
   32.17 +	(Simp_tac 1)
   32.18  	]);
   32.19  
   32.20  (** --------- proves about iterations of p and q ---------- **)
   32.21  
   32.22 +val HOLCF_ss = simpset_of "HOLCF";
   32.23 +
   32.24  val hoare_lemma9 = prove_goal Hoare.thy 
   32.25  "(! m. m< Suc k --> b1`(iterate m g x)=TT) -->\
   32.26  \  p`(iterate k g x)=p`x"
   32.27   (fn prems =>
   32.28  	[
   32.29  	(nat_ind_tac "k" 1),
   32.30 -	(simp_tac iterate_ss 1),
   32.31 -	(simp_tac iterate_ss 1),
   32.32 +	(simp_tac (!simpset delsimps [less_Suc_eq]) 1),
   32.33 +	(simp_tac (!simpset delsimps [less_Suc_eq]) 1),
   32.34  	(strip_tac 1),
   32.35  	(res_inst_tac [("s","p`(iterate k1 g x)")] trans 1),
   32.36  	(rtac trans 1),
   32.37 @@ -152,24 +154,24 @@
   32.38  	(res_inst_tac [("s","TT"),("t","b1`(iterate k1 g x)")] ssubst 1),
   32.39  	(rtac mp 1),
   32.40  	(etac spec 1),
   32.41 -	(simp_tac nat_ss 1),
   32.42 +	(Simp_tac 1),
   32.43  	(simp_tac HOLCF_ss 1),
   32.44  	(etac mp 1),
   32.45  	(strip_tac 1),
   32.46  	(rtac mp 1),
   32.47  	(etac spec 1),
   32.48  	(etac less_trans 1),
   32.49 -	(simp_tac nat_ss 1)
   32.50 +	(Simp_tac 1)
   32.51  	]);
   32.52 -
   32.53 +trace_simp := false;
   32.54  val hoare_lemma24 = prove_goal Hoare.thy 
   32.55  "(! m. m< Suc k --> b1`(iterate m g x)=TT) --> \
   32.56  \ q`(iterate k g x)=q`x"
   32.57   (fn prems =>
   32.58  	[
   32.59  	(nat_ind_tac "k" 1),
   32.60 -	(simp_tac iterate_ss 1),
   32.61 -	(simp_tac iterate_ss 1),
   32.62 +	(simp_tac (!simpset delsimps [less_Suc_eq]) 1),
   32.63 +	(simp_tac (!simpset delsimps [less_Suc_eq]) 1),
   32.64  	(strip_tac 1),
   32.65  	(res_inst_tac [("s","q`(iterate k1 g x)")] trans 1),
   32.66  	(rtac trans 1),
   32.67 @@ -177,14 +179,14 @@
   32.68  	(res_inst_tac [("s","TT"),("t","b1`(iterate k1 g x)")] ssubst 1),
   32.69  	(rtac mp 1),
   32.70  	(etac spec 1),
   32.71 -	(simp_tac nat_ss 1),
   32.72 +	(Simp_tac 1),
   32.73  	(simp_tac HOLCF_ss 1),
   32.74  	(etac mp 1),
   32.75  	(strip_tac 1),
   32.76  	(rtac mp 1),
   32.77  	(etac spec 1),
   32.78  	(etac less_trans 1),
   32.79 -	(simp_tac nat_ss 1)
   32.80 +	(Simp_tac 1)
   32.81  	]);
   32.82  
   32.83  (* -------- results about p for case (? k. b1`(iterate k g x)~=TT) ------- *)
   32.84 @@ -207,15 +209,15 @@
   32.85  	(cut_facts_tac prems 1),
   32.86  	(res_inst_tac [("n","k")] natE 1),
   32.87  	(hyp_subst_tac 1),
   32.88 -	(simp_tac iterate_ss 1),
   32.89 +	(Simp_tac 1),
   32.90  	(strip_tac 1),
   32.91  	(etac conjE 1),
   32.92  	(rtac trans 1),
   32.93  	(rtac p_def3 1),
   32.94 -	(asm_simp_tac HOLCF_ss  1),
   32.95 -	(eres_inst_tac [("s","0"),("t","theleast(%n. b1`(iterate n g x) ~= TT)")]
   32.96 -	subst 1),
   32.97 -	(simp_tac iterate_ss 1),
   32.98 +	(asm_simp_tac HOLCF_ss 1),
   32.99 +	(eres_inst_tac
  32.100 +           [("s","0"),("t","theleast(%n. b1`(iterate n g x) ~= TT)")] subst 1),
  32.101 +	(Simp_tac 1),
  32.102  	(hyp_subst_tac 1),
  32.103  	(strip_tac 1),
  32.104  	(etac conjE 1),
  32.105 @@ -228,12 +230,13 @@
  32.106  	(rtac (hoare_lemma8 RS spec RS mp) 1),
  32.107  	(atac 1),
  32.108  	(atac 1),
  32.109 -	(simp_tac nat_ss 1),
  32.110 +	(Simp_tac 1),
  32.111  	(simp_tac HOLCF_ss 1),
  32.112  	(rtac trans 1),
  32.113  	(rtac p_def3 1),
  32.114 -	(simp_tac (HOLCF_ss addsimps [iterate_Suc RS sym]) 1),
  32.115 -	(eres_inst_tac [("s","FF")]	ssubst 1),
  32.116 +	(simp_tac (!simpset delsimps [iterate_Suc]
  32.117 +                            addsimps [iterate_Suc RS sym]) 1),
  32.118 +	(eres_inst_tac [("s","FF")] ssubst 1),
  32.119  	(simp_tac HOLCF_ss 1)
  32.120  	]);
  32.121  
  32.122 @@ -246,14 +249,14 @@
  32.123  	(cut_facts_tac prems 1),
  32.124  	(res_inst_tac [("n","k")] natE 1),
  32.125  	(hyp_subst_tac 1),
  32.126 -	(simp_tac iterate_ss 1),
  32.127 +	(Simp_tac 1),
  32.128  	(strip_tac 1),
  32.129  	(etac conjE 1),
  32.130  	(rtac trans 1),
  32.131  	(rtac p_def3 1),
  32.132 -	(asm_simp_tac HOLCF_ss  1),
  32.133 +	(asm_simp_tac HOLCF_ss 1),
  32.134  	(hyp_subst_tac 1),
  32.135 -	(simp_tac iterate_ss 1),
  32.136 +	(Simp_tac 1),
  32.137  	(strip_tac 1),
  32.138  	(etac conjE 1),
  32.139  	(rtac trans 1),
  32.140 @@ -266,11 +269,11 @@
  32.141  	(rtac (hoare_lemma8 RS spec RS mp) 1),
  32.142  	(atac 1),
  32.143  	(atac 1),
  32.144 -	(simp_tac nat_ss 1),
  32.145 -	(asm_simp_tac HOLCF_ss  1),
  32.146 +	(Simp_tac 1),
  32.147 +	(asm_simp_tac HOLCF_ss 1),
  32.148  	(rtac trans 1),
  32.149  	(rtac p_def3 1),
  32.150 -	(asm_simp_tac HOLCF_ss  1)
  32.151 +	(asm_simp_tac HOLCF_ss 1)
  32.152  	]);
  32.153  
  32.154  (* -------- results about p for case  (! k. b1`(iterate k g x)=TT) ------- *)
  32.155 @@ -289,7 +292,7 @@
  32.156  	(rtac allI 1),
  32.157  	(rtac (strict_fapp1 RS ssubst) 1),
  32.158  	(rtac refl 1),
  32.159 -	(simp_tac iterate_ss 1),
  32.160 +	(Simp_tac 1),
  32.161  	(rtac allI 1),
  32.162  	(res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1),
  32.163  	(etac spec 1),
  32.164 @@ -324,10 +327,10 @@
  32.165  	(rtac (strict_fapp1 RS ssubst) 1),
  32.166  	(rtac refl 1),
  32.167  	(rtac allI 1),
  32.168 -	(simp_tac iterate_ss 1),
  32.169 +	(Simp_tac 1),
  32.170  	(res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1),
  32.171  	(etac spec 1),
  32.172 -	(asm_simp_tac HOLCF_ss  1),
  32.173 +	(asm_simp_tac HOLCF_ss 1),
  32.174  	(rtac (iterate_Suc RS subst) 1),
  32.175  	(etac spec 1)
  32.176  	]);
  32.177 @@ -366,10 +369,10 @@
  32.178  	(rtac (strict_fapp1 RS ssubst) 1),
  32.179  	(rtac refl 1),
  32.180  	(rtac allI 1),
  32.181 -	(simp_tac iterate_ss 1),
  32.182 +	(Simp_tac 1),
  32.183  	(res_inst_tac [("s","TT"),("t","b1`(iterate k g (x::'a))")] ssubst 1),
  32.184  	(etac spec 1),
  32.185 -	(asm_simp_tac HOLCF_ss  1),
  32.186 +	(asm_simp_tac HOLCF_ss 1),
  32.187  	(rtac (iterate_Suc RS subst) 1),
  32.188  	(etac spec 1)
  32.189  	]);
  32.190 @@ -389,7 +392,7 @@
  32.191  	[
  32.192  	(cut_facts_tac prems 1),
  32.193  	(rtac (q_def3 RS ssubst) 1),
  32.194 -	(asm_simp_tac HOLCF_ss  1)
  32.195 +	(asm_simp_tac HOLCF_ss 1)
  32.196  	]);
  32.197  
  32.198  (* -------- results about q for case (? k. b1`(iterate k g x) ~= TT) ------- *)
  32.199 @@ -411,7 +414,7 @@
  32.200  	(res_inst_tac [("n","k")] natE 1),
  32.201  	(hyp_subst_tac 1),
  32.202  	(strip_tac 1),
  32.203 -	(simp_tac iterate_ss 1),
  32.204 +	(Simp_tac 1),
  32.205  	(hyp_subst_tac 1),
  32.206  	(strip_tac 1),
  32.207  	(etac conjE 1),
  32.208 @@ -425,8 +428,8 @@
  32.209  	(rtac (hoare_lemma8 RS spec RS mp) 1),
  32.210  	(atac 1),
  32.211  	(atac 1),
  32.212 -	(simp_tac nat_ss 1),
  32.213 -	(simp_tac (HOLCF_ss addsimps [iterate_Suc]) 1)
  32.214 +	(Simp_tac 1),
  32.215 +	(simp_tac HOLCF_ss 1)
  32.216  	]);
  32.217  
  32.218  
  32.219 @@ -439,13 +442,13 @@
  32.220  	(cut_facts_tac prems 1),
  32.221  	(res_inst_tac [("n","k")] natE 1),
  32.222  	(hyp_subst_tac 1),
  32.223 -	(simp_tac iterate_ss 1),
  32.224 +	(Simp_tac 1),
  32.225  	(strip_tac 1),
  32.226  	(etac conjE 1),
  32.227  	(rtac (q_def3 RS ssubst) 1),
  32.228 -	(asm_simp_tac HOLCF_ss  1),
  32.229 +	(asm_simp_tac HOLCF_ss 1),
  32.230  	(hyp_subst_tac 1),
  32.231 -	(simp_tac iterate_ss 1),
  32.232 +	(Simp_tac 1),
  32.233  	(strip_tac 1),
  32.234  	(etac conjE 1),
  32.235  	(rtac trans 1),
  32.236 @@ -458,11 +461,11 @@
  32.237  	(rtac (hoare_lemma8 RS spec RS mp) 1),
  32.238  	(atac 1),
  32.239  	(atac 1),
  32.240 -	(simp_tac nat_ss 1),
  32.241 +	(Simp_tac 1),
  32.242  	(asm_simp_tac HOLCF_ss 1),
  32.243  	(rtac trans 1),
  32.244  	(rtac q_def3 1),
  32.245 -	(asm_simp_tac HOLCF_ss  1)
  32.246 +	(asm_simp_tac HOLCF_ss 1)
  32.247  	]);
  32.248  
  32.249  (* ------- (! k. b1`(iterate k g x)=TT) ==> q o p = q   ----- *)
    33.1 --- a/src/HOLCF/ex/Loop.ML	Wed Oct 04 13:12:14 1995 +0100
    33.2 +++ b/src/HOLCF/ex/Loop.ML	Wed Oct 04 14:01:44 1995 +0100
    33.3 @@ -16,14 +16,14 @@
    33.4  "step`b`g`x = If b`x then g`x else x fi"
    33.5   (fn prems =>
    33.6  	[
    33.7 -	(simp_tac Cfun_ss 1)
    33.8 +	(Simp_tac 1)
    33.9  	]);
   33.10  
   33.11  val while_def2 = prove_goalw Loop.thy [while_def]
   33.12  "while`b`g = fix`(LAM f x. If b`x then f`(g`x) else x fi)"
   33.13   (fn prems =>
   33.14  	[
   33.15 -	(simp_tac Cfun_ss 1)
   33.16 +	(Simp_tac 1)
   33.17  	]);
   33.18  
   33.19  
   33.20 @@ -36,15 +36,17 @@
   33.21   (fn prems =>
   33.22  	[
   33.23  	(fix_tac5  while_def2 1),
   33.24 -	(simp_tac Cfun_ss 1)
   33.25 +	(Simp_tac 1)
   33.26  	]);
   33.27  
   33.28 +val HOLCF_ss = simpset_of "HOLCF";
   33.29 +
   33.30  val while_unfold2 = prove_goal Loop.thy 
   33.31  	"!x.while`b`g`x = while`b`g`(iterate k (step`b`g) x)"
   33.32   (fn prems =>
   33.33  	[
   33.34  	(nat_ind_tac "k" 1),
   33.35 -	(simp_tac (HOLCF_ss addsimps [iterate_0,iterate_Suc]) 1),
   33.36 +	(simp_tac HOLCF_ss 1),
   33.37  	(rtac allI 1),
   33.38  	(rtac trans 1),
   33.39  	(rtac (while_unfold RS ssubst) 1),
   33.40 @@ -74,7 +76,7 @@
   33.41  	(res_inst_tac [("s",
   33.42  		"while`b`g`(iterate (Suc 0) (step`b`g) x)")] trans 1),
   33.43  	(rtac (while_unfold2 RS spec) 1),
   33.44 -	(simp_tac iterate_ss 1)
   33.45 +	(Simp_tac 1)
   33.46  	]);
   33.47  
   33.48  
   33.49 @@ -87,7 +89,7 @@
   33.50   (fn prems =>
   33.51  	[
   33.52  	(cut_facts_tac prems 1),
   33.53 -	(simp_tac iterate_ss 1),
   33.54 +	(Simp_tac 1),
   33.55  	(rtac trans 1),
   33.56  	(rtac step_def2 1),
   33.57  	(asm_simp_tac HOLCF_ss 1),
   33.58 @@ -117,21 +119,23 @@
   33.59  	[
   33.60  	(cut_facts_tac prems 1),
   33.61  	(nat_ind_tac "k" 1),
   33.62 -	(asm_simp_tac iterate_ss 1),
   33.63 +	(Asm_simp_tac 1),
   33.64  	(strip_tac 1),
   33.65 -	(simp_tac (iterate_ss addsimps [step_def2]) 1),
   33.66 +	(simp_tac (!simpset addsimps [step_def2]) 1),
   33.67  	(res_inst_tac [("p","b`(iterate k1 (step`b`g) x)")] trE 1),
   33.68  	(etac notE 1),
   33.69 -	(asm_simp_tac (HOLCF_ss addsimps [step_def2,iterate_Suc] ) 1),
   33.70 -	(asm_simp_tac HOLCF_ss  1),
   33.71 +	(asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1),
   33.72 +	(asm_simp_tac HOLCF_ss 1),
   33.73  	(rtac mp 1),
   33.74 -	(etac spec  1),
   33.75 -	(asm_simp_tac (HOLCF_ss addsimps [loop_lemma2] ) 1),
   33.76 +	(etac spec 1),
   33.77 +	(asm_simp_tac (HOLCF_ss delsimps [iterate_Suc]
   33.78 +                                addsimps [loop_lemma2] ) 1),
   33.79  	(res_inst_tac [("s","iterate (Suc k1) (step`b`g) x"),
   33.80  		("t","g`(iterate k1 (step`b`g) x)")] ssubst 1),
   33.81  	(atac 2),
   33.82 -	(asm_simp_tac (HOLCF_ss addsimps [iterate_Suc,step_def2] ) 1),
   33.83 -	(asm_simp_tac (HOLCF_ss addsimps [loop_lemma2] ) 1)
   33.84 +	(asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1),
   33.85 +	(asm_simp_tac (HOLCF_ss delsimps [iterate_Suc]
   33.86 +                                addsimps [loop_lemma2] ) 1)
   33.87  	]);
   33.88  
   33.89  
   33.90 @@ -140,16 +144,16 @@
   33.91   (fn prems =>
   33.92  	[
   33.93  	(nat_ind_tac "k" 1),
   33.94 -	(simp_tac iterate_ss 1),
   33.95 +	(Simp_tac 1),
   33.96  	(strip_tac 1),
   33.97  	(rtac (while_unfold RS ssubst) 1),
   33.98 -	(asm_simp_tac HOLCF_ss  1),
   33.99 +	(asm_simp_tac HOLCF_ss 1),
  33.100  	(rtac allI 1),
  33.101  	(rtac (iterate_Suc2 RS ssubst) 1),
  33.102  	(strip_tac 1),
  33.103  	(rtac trans 1),
  33.104  	(rtac while_unfold3 1),
  33.105 -	(asm_simp_tac HOLCF_ss  1)
  33.106 +	(asm_simp_tac HOLCF_ss 1)
  33.107  	]);
  33.108  
  33.109  val loop_lemma5 = prove_goal Loop.thy
  33.110 @@ -163,12 +167,12 @@
  33.111  	(rtac (allI RS adm_all) 1),
  33.112  	(rtac adm_eq 1),
  33.113  	(cont_tacR 1),
  33.114 -	(simp_tac HOLCF_ss  1),
  33.115 +	(Simp_tac  1),
  33.116  	(rtac allI 1),
  33.117 -	(simp_tac HOLCF_ss  1),
  33.118 +	(Simp_tac  1),
  33.119  	(res_inst_tac [("p","b`(iterate m (step`b`g) x)")] trE 1),
  33.120 -	(asm_simp_tac HOLCF_ss  1),
  33.121 -	(asm_simp_tac HOLCF_ss  1),
  33.122 +	(asm_simp_tac HOLCF_ss 1),
  33.123 +	(asm_simp_tac HOLCF_ss 1),
  33.124  	(res_inst_tac [("s","xa`(iterate (Suc m) (step`b`g) x)")] trans 1),
  33.125  	(etac spec 2),
  33.126  	(rtac cfun_arg_cong 1),