src/HOLCF/Sprod3.ML

 	(rtac (monofun_Isfst RS ch2ch_monofun) 1),
 	(rtac ch2ch_fun 1),
 	(rtac (monofun_Ispair1 RS ch2ch_monofun) 1),
 	(atac 1),
 	(rtac allI 1),
-	(asm_simp_tac Sprod_ss 1),
+	(Asm_simp_tac 1),
 	(rtac sym 1),
 	(rtac lub_chain_maxelem 1),
 	(res_inst_tac [("P","%j.~Y(j)=UU")] exE 1),
 	(rtac (notall2ex RS iffD1) 1),
 	(res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1),

 	(atac 1),
 	(rtac exI 1),
 	(etac Issnd2 1),
 	(rtac allI 1),
 	(res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1),
-	(asm_simp_tac Sprod_ss  1),
-	(rtac refl_less 1),
+	(Asm_simp_tac 1),
 	(res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
 	(etac sym 1),
-	(asm_simp_tac Sprod_ss  1),
-	(rtac minimal 1)
+	(Asm_simp_tac 1)
 	]);
 
 qed_goal "sprod3_lemma2" Sprod3.thy 
 "[| is_chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
 \   Ispair (lub(range Y)) x =\

 	(rtac strict_Ispair1 1),
 	(rtac (strict_Ispair RS sym) 1),
 	(rtac disjI1 1),
 	(rtac chain_UU_I_inverse 1),
 	(rtac allI 1),
-	(asm_simp_tac Sprod_ss  1),
+	(Asm_simp_tac  1),
 	(etac (chain_UU_I RS spec) 1),
 	(atac 1)
 	]);
 
 

 	(rtac strict_Ispair2 1),
 	(rtac (strict_Ispair RS sym) 1),
 	(rtac disjI1 1),
 	(rtac chain_UU_I_inverse 1),
 	(rtac allI 1),
-	(simp_tac Sprod_ss  1)
+	(Simp_tac  1)
 	]);
 
 
 qed_goal "contlub_Ispair1" Sprod3.thy "contlub(Ispair)"
 (fn prems =>

 	(atac 1),
 	(rtac exI 1),
 	(etac Isfst2 1),
 	(rtac allI 1),
 	(res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1),
-	(asm_simp_tac Sprod_ss 1),
-	(rtac refl_less 1),
+	(Asm_simp_tac 1),
 	(res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
 	(etac sym 1),
-	(asm_simp_tac Sprod_ss  1),
-	(rtac minimal 1),
+	(Asm_simp_tac  1),
 	(rtac lub_equal 1),
 	(atac 1),
 	(rtac (monofun_Issnd RS ch2ch_monofun) 1),
 	(rtac (monofun_Ispair2 RS ch2ch_monofun) 1),
 	(atac 1),
 	(rtac allI 1),
-	(asm_simp_tac Sprod_ss 1)
+	(Asm_simp_tac 1)
 	]);
 
 qed_goal "sprod3_lemma5" Sprod3.thy 
 "[| is_chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
 \         Ispair x (lub(range Y)) =\

 	(rtac strict_Ispair2 1),
 	(rtac (strict_Ispair RS sym) 1),
 	(rtac disjI2 1),
 	(rtac chain_UU_I_inverse 1),
 	(rtac allI 1),
-	(asm_simp_tac Sprod_ss  1),
+	(Asm_simp_tac  1),
 	(etac (chain_UU_I RS spec) 1),
 	(atac 1)
 	]);
 
 qed_goal "sprod3_lemma6" Sprod3.thy 

 	(rtac strict_Ispair1 1),
 	(rtac (strict_Ispair RS sym) 1),
 	(rtac disjI1 1),
 	(rtac chain_UU_I_inverse 1),
 	(rtac allI 1),
-	(simp_tac Sprod_ss  1)
+	(Simp_tac 1)
 	]);
 
 qed_goal "contlub_Ispair2" Sprod3.thy "contlub(Ispair(x))"
 (fn prems =>
 	[

 	(strip_tac 1),
 	(rtac (lub_sprod RS thelubI RS ssubst) 1),
 	(atac 1),
 	(res_inst_tac [("Q","lub(range(%i. Issnd(Y(i))))=UU")]	
 		(excluded_middle RS disjE) 1),
-	(asm_simp_tac Sprod_ss  1),
+	(Asm_simp_tac  1),
 	(res_inst_tac [("s","UU"),("t","lub(range(%i. Issnd(Y(i))))")]
 		ssubst 1),
 	(atac 1),
 	(rtac trans 1),
-	(asm_simp_tac Sprod_ss  1),
+	(Asm_simp_tac  1),
 	(rtac sym 1),
 	(rtac chain_UU_I_inverse 1),
 	(rtac allI 1),
 	(rtac strict_Isfst 1),
 	(rtac swap 1),

 	(strip_tac 1),
 	(rtac (lub_sprod RS thelubI RS ssubst) 1),
 	(atac 1),
 	(res_inst_tac [("Q","lub(range(%i. Isfst(Y(i))))=UU")]
 	 (excluded_middle RS disjE) 1),
-	(asm_simp_tac Sprod_ss  1),
+	(Asm_simp_tac  1),
 	(res_inst_tac [("s","UU"),("t","lub(range(%i. Isfst(Y(i))))")] 
 		ssubst 1),
 	(atac 1),
-	(asm_simp_tac Sprod_ss  1),
+	(Asm_simp_tac  1),
 	(rtac sym 1),
 	(rtac chain_UU_I_inverse 1),
 	(rtac allI 1),
 	(rtac strict_Issnd 1),
 	(rtac swap 1),

 
 (* ------------------------------------------------------------------------ *)
 (* install simplifier for Sprod                                             *)
 (* ------------------------------------------------------------------------ *)
 
-val Sprod_rews = [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2,
-		strict_ssnd1,strict_ssnd2,sfst2,ssnd2,
-		ssplit1,ssplit2];
-
-val Sprod_ss = Cfun_ss addsimps Sprod_rews;
-
-
+Addsimps [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2,
+	  strict_ssnd1,strict_ssnd2,sfst2,ssnd2,
+	  ssplit1,ssplit2];
+
+