src/HOLCF/Ssum3.ML

 	(atac 1),
 	(rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
 	(etac (monofun_Isinl RS ch2ch_monofun) 1),
 	(rtac allI 1),
 	(res_inst_tac [("Q","Y(k)=UU")] classical2 1),
-	(asm_simp_tac Ssum_ss 1),
-	(asm_simp_tac Ssum_ss 1)
+	(Asm_simp_tac 1),
+	(Asm_simp_tac 1)
 	]);
 
 qed_goal "contlub_Isinr" Ssum3.thy "contlub(Isinr)"
  (fn prems =>
 	[

 	(atac 1),
 	(rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
 	(etac (monofun_Isinr RS ch2ch_monofun) 1),
 	(rtac allI 1),
 	(res_inst_tac [("Q","Y(k)=UU")] classical2 1),
-	(asm_simp_tac Ssum_ss 1),
-	(asm_simp_tac Ssum_ss 1)
+	(Asm_simp_tac 1),
+	(Asm_simp_tac 1)
 	]);
 
 qed_goal "cont_Isinl" Ssum3.thy "cont(Isinl)"
  (fn prems =>
 	[

 	(rtac ch2ch_fun 2),
 	(etac (monofun_Iwhen1 RS ch2ch_monofun) 2),
 	(rtac (expand_fun_eq RS iffD2) 1),
 	(strip_tac 1),
 	(res_inst_tac [("p","xa")] IssumE 1),
-	(asm_simp_tac Ssum_ss 1),
+	(Asm_simp_tac 1),
 	(rtac (lub_const RS thelubI RS sym) 1),
-	(asm_simp_tac Ssum_ss 1),
+	(Asm_simp_tac 1),
 	(etac contlub_cfun_fun 1),
-	(asm_simp_tac Ssum_ss 1),
+	(Asm_simp_tac 1),
 	(rtac (lub_const RS thelubI RS sym) 1)
 	]);
 
 qed_goal "contlub_Iwhen2" Ssum3.thy "contlub(Iwhen(f))"
  (fn prems =>

 	(rtac (thelub_fun RS sym) 2),
 	(etac (monofun_Iwhen2 RS ch2ch_monofun) 2),
 	(rtac (expand_fun_eq RS iffD2) 1),
 	(strip_tac 1),
 	(res_inst_tac [("p","x")] IssumE 1),
-	(asm_simp_tac Ssum_ss 1),
+	(Asm_simp_tac 1),
 	(rtac (lub_const RS thelubI RS sym) 1),
-	(asm_simp_tac Ssum_ss 1),
+	(Asm_simp_tac 1),
 	(rtac (lub_const RS thelubI RS sym) 1),
-	(asm_simp_tac Ssum_ss 1),
+	(Asm_simp_tac 1),
 	(etac contlub_cfun_fun 1)
 	]);
 
 (* ------------------------------------------------------------------------ *)
 (* continuity for Iwhen in its third argument                               *)

 "[| is_chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\
 \   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(asm_simp_tac Ssum_ss 1),
+	(Asm_simp_tac 1),
 	(rtac (chain_UU_I_inverse RS sym) 1),
 	(rtac allI 1),
 	(res_inst_tac [("s","Isinl(UU)"),("t","Y(i)")] subst 1),
 	(rtac (inst_ssum_pcpo RS subst) 1),
 	(rtac (chain_UU_I RS spec RS sym) 1),
 	(atac 1),
 	(etac (inst_ssum_pcpo RS ssubst) 1),
-	(asm_simp_tac Ssum_ss 1)
+	(Asm_simp_tac 1)
 	]);
 
 qed_goal "ssum_lemma12" Ssum3.thy 
 "[| is_chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==>\
 \   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(asm_simp_tac Ssum_ss 1),
+	(Asm_simp_tac 1),
 	(res_inst_tac [("t","x")] subst 1),
 	(rtac inject_Isinl 1),
 	(rtac trans 1),
 	(atac 2),
 	(rtac (thelub_ssum1a RS sym) 1),

 	(fast_tac HOL_cs 1),
 	(rtac (inst_ssum_pcpo RS ssubst) 1),
 	(res_inst_tac [("t","Y(i)")] ssubst 1),
 	(atac 1),
 	(fast_tac HOL_cs 1),
-	(simp_tac Cfun_ss 1),
+	(Simp_tac 1),
 	(rtac (monofun_fapp2 RS ch2ch_monofun) 1),
 	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
 	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
 	]);
 

 "[| is_chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==>\
 \   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(asm_simp_tac Ssum_ss 1),
+	(Asm_simp_tac 1),
 	(res_inst_tac [("t","x")] subst 1),
 	(rtac inject_Isinr 1),
 	(rtac trans 1),
 	(atac 2),
 	(rtac (thelub_ssum1b RS sym) 1),

 	(rtac (inst_ssum_pcpo RS ssubst) 1),
 	(rtac (strict_IsinlIsinr RS ssubst) 1),
 	(res_inst_tac [("t","Y(i)")] ssubst 1),
 	(atac 1),
 	(fast_tac HOL_cs 1),
-	(simp_tac Cfun_ss 1),
+	(Simp_tac 1),
 	(rtac (monofun_fapp2 RS ch2ch_monofun) 1),
 	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
 	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
 	]);
 

 (* ------------------------------------------------------------------------ *)
 
 qed_goalw "strict_sinl" Ssum3.thy [sinl_def] "sinl`UU =UU"
  (fn prems =>
 	[
-	(simp_tac (Ssum_ss addsimps [cont_Isinl]) 1),
+	(simp_tac (!simpset addsimps [cont_Isinl]) 1),
 	(rtac (inst_ssum_pcpo RS sym) 1)
 	]);
 
 qed_goalw "strict_sinr" Ssum3.thy [sinr_def] "sinr`UU=UU"
  (fn prems =>
 	[
-	(simp_tac (Ssum_ss addsimps [cont_Isinr]) 1),
+	(simp_tac (!simpset addsimps [cont_Isinr]) 1),
 	(rtac (inst_ssum_pcpo RS sym) 1)
 	]);
 
 qed_goalw "noteq_sinlsinr" Ssum3.thy [sinl_def,sinr_def] 
 	"sinl`a=sinr`b ==> a=UU & b=UU"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac noteq_IsinlIsinr 1),
 	(etac box_equals 1),
-	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1),
-	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1)
+	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
+	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1)
 	]);
 
 qed_goalw "inject_sinl" Ssum3.thy [sinl_def,sinr_def] 
 	"sinl`a1=sinl`a2==> a1=a2"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac inject_Isinl 1),
 	(etac box_equals 1),
-	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1),
-	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1)
+	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
+	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1)
 	]);
 
 qed_goalw "inject_sinr" Ssum3.thy [sinl_def,sinr_def] 
 	"sinr`a1=sinr`a2==> a1=a2"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac inject_Isinr 1),
 	(etac box_equals 1),
-	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1),
-	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1)
+	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
+	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1)
 	]);
 
 
 qed_goal "defined_sinl" Ssum3.thy  
 	"x~=UU ==> sinl`x ~= UU"

 
 qed_goalw "Exh_Ssum1" Ssum3.thy [sinl_def,sinr_def] 
 	"z=UU | (? a. z=sinl`a & a~=UU) | (? b. z=sinr`b & b~=UU)"
  (fn prems =>
 	[
-	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1),
+	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
 	(rtac (inst_ssum_pcpo RS ssubst) 1),
 	(rtac Exh_Ssum 1)
 	]);
 
 

 	(resolve_tac prems 1),
 	(rtac (inst_ssum_pcpo RS ssubst) 1),
 	(atac 1),
 	(resolve_tac prems 1),
 	(atac 2),
-	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1),
+	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
 	(resolve_tac prems 1),
 	(atac 2),
-	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1)
+	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1)
 	]);
 
 
 qed_goalw "ssumE2" Ssum3.thy [sinl_def,sinr_def] 
       "[|!!x.[|p=sinl`x|] ==> Q;\

 	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
 		cont_Iwhen3,cont2cont_CF1L]) 1)),
 	(rtac (beta_cfun RS ssubst) 1),
 	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
 		cont_Iwhen3,cont2cont_CF1L]) 1)),
-	(simp_tac Ssum_ss  1)
+	(Simp_tac 1)
 	]);
 
 qed_goalw "sswhen2" Ssum3.thy [sswhen_def,sinl_def,sinr_def] 
 	"x~=UU==> sswhen`f`g`(sinl`x) = f`x"
  (fn prems =>

 	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
 		cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
 	(rtac (beta_cfun RS ssubst) 1),
 	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
 		cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
-	(asm_simp_tac Ssum_ss  1)
+	(Asm_simp_tac  1)
 	]);
 
 
 
 qed_goalw "sswhen3" Ssum3.thy [sswhen_def,sinl_def,sinr_def] 

 	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
 		cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
 	(rtac (beta_cfun RS ssubst) 1),
 	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
 		cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
-	(asm_simp_tac Ssum_ss  1)
+	(Asm_simp_tac 1)
 	]);
 
 
 qed_goalw "less_ssum4a" Ssum3.thy [sinl_def,sinr_def] 
 	"(sinl`x << sinl`y) = (x << y)"

 qed_goalw "ssum_chainE" Ssum3.thy [sinl_def,sinr_def] 
 	"is_chain(Y) ==> (!i.? x.(Y i)=sinl`x)|(!i.? y.(Y i)=sinr`y)"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1),
+	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
 	(etac ssum_lemma4 1)
 	]);
 
 
 qed_goalw "thelub_ssum2a" Ssum3.thy [sinl_def,sinr_def,sswhen_def] 

 	(etac allE 1),
 	(etac exE 1),
 	(rtac exI 1),
 	(etac box_equals 1),
 	(rtac refl 1),
-	(asm_simp_tac (Ssum_ss addsimps [cont_Isinl]) 1)
+	(asm_simp_tac (!simpset addsimps [cont_Isinl]) 1)
 	]);
 
 qed_goalw "thelub_ssum2b" Ssum3.thy [sinl_def,sinr_def,sswhen_def] 
 "[| is_chain(Y); !i.? x. Y(i) = sinr`x |] ==>\ 
 \   lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x.x)`(Y i))))"

 	(etac allE 1),
 	(etac exE 1),
 	(rtac exI 1),
 	(etac box_equals 1),
 	(rtac refl 1),
-	(asm_simp_tac (Ssum_ss addsimps 
+	(asm_simp_tac (!simpset addsimps 
 	[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
 	cont_Iwhen3]) 1)
 	]);
 
 qed_goalw "thelub_ssum2a_rev" Ssum3.thy [sinl_def,sinr_def] 
 	"[| is_chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x.Y(i)=sinl`x"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(asm_simp_tac (Ssum_ss addsimps 
+	(asm_simp_tac (!simpset addsimps 
 	[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
 	cont_Iwhen3]) 1),
 	(etac ssum_lemma9 1),
-	(asm_simp_tac (Ssum_ss addsimps 
+	(asm_simp_tac (!simpset addsimps 
 	[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
 	cont_Iwhen3]) 1)
 	]);
 
 qed_goalw "thelub_ssum2b_rev" Ssum3.thy [sinl_def,sinr_def] 
 	"[| is_chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x.Y(i)=sinr`x"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(asm_simp_tac (Ssum_ss addsimps 
+	(asm_simp_tac (!simpset addsimps 
 	[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
 	cont_Iwhen3]) 1),
 	(etac ssum_lemma10 1),
-	(asm_simp_tac (Ssum_ss addsimps 
+	(asm_simp_tac (!simpset addsimps 
 	[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
 	cont_Iwhen3]) 1)
 	]);
 
 qed_goal "thelub_ssum3" Ssum3.thy  

 qed_goal "sswhen4" Ssum3.thy  
 	"sswhen`sinl`sinr`z=z"
  (fn prems =>
 	[
 	(res_inst_tac [("p","z")] ssumE 1),
-	(asm_simp_tac (Cfun_ss addsimps [sswhen1,sswhen2,sswhen3]) 1),
-	(asm_simp_tac (Cfun_ss addsimps [sswhen1,sswhen2,sswhen3]) 1),
-	(asm_simp_tac (Cfun_ss addsimps [sswhen1,sswhen2,sswhen3]) 1)
+	(asm_simp_tac (!simpset addsimps [sswhen1,sswhen2,sswhen3]) 1),
+	(asm_simp_tac (!simpset addsimps [sswhen1,sswhen2,sswhen3]) 1),
+	(asm_simp_tac (!simpset addsimps [sswhen1,sswhen2,sswhen3]) 1)
 	]);
 
 
 (* ------------------------------------------------------------------------ *)
 (* install simplifier for Ssum                                              *)
 (* ------------------------------------------------------------------------ *)
 
-val Ssum_rews = [strict_sinl,strict_sinr,sswhen1,sswhen2,sswhen3];
-val Ssum_ss = Cfun_ss addsimps Ssum_rews;
+Addsimps [strict_sinl,strict_sinr,sswhen1,sswhen2,sswhen3];