# HG changeset patch
# User regensbu
# Date 813322545 -3600
# Node ID caef3601c0b2fffd590d679da462e6bc8e8b56c5
# Parent  42ccfd3e1fb428486a214ec99aa0bff96610fa49
corrected some errors that occurred after introduction of local simpsets

diff -r 42ccfd3e1fb4 -r caef3601c0b2 src/HOLCF/Lift1.ML
--- a/src/HOLCF/Lift1.ML	Mon Oct 09 14:57:55 1995 +0100
+++ b/src/HOLCF/Lift1.ML	Tue Oct 10 11:55:45 1995 +0100
@@ -84,7 +84,7 @@
 	(rtac refl 1)
 	]);
 
-Addsimps [Ilift1,Ilift2];
+val Lift0_ss = (simpset_of "Cfun3") addsimps [Ilift1,Ilift2];
 
 qed_goalw "less_lift1a"  Lift1.thy [less_lift_def,UU_lift_def]
 	"less_lift(UU_lift)(z)"
diff -r 42ccfd3e1fb4 -r caef3601c0b2 src/HOLCF/Lift2.ML
--- a/src/HOLCF/Lift2.ML	Mon Oct 09 14:57:55 1995 +0100
+++ b/src/HOLCF/Lift2.ML	Tue Oct 10 11:55:45 1995 +0100
@@ -55,8 +55,8 @@
 	(rtac (less_fun RS iffD2) 1),
 	(strip_tac 1),
 	(res_inst_tac [("p","xa")] liftE 1),
-	(Asm_simp_tac 1),
-	(Asm_simp_tac 1),
+        (asm_simp_tac Lift0_ss 1),
+        (asm_simp_tac Lift0_ss 1),
 	(etac monofun_cfun_fun 1)
 	]);
 
@@ -65,14 +65,14 @@
 	[
 	(strip_tac 1),
 	(res_inst_tac [("p","x")] liftE 1),
-	(Asm_simp_tac 1),
-	(Asm_simp_tac 1),
+        (asm_simp_tac Lift0_ss 1),
+        (asm_simp_tac Lift0_ss 1),
 	(res_inst_tac [("p","y")] liftE 1),
 	(hyp_subst_tac 1),
 	(rtac notE 1),
 	(rtac less_lift2b 1),
 	(atac 1),
-	(Asm_simp_tac 1),
+        (asm_simp_tac Lift0_ss 1),
 	(rtac monofun_cfun_arg 1),
 	(hyp_subst_tac 1),
 	(etac (less_lift2c  RS iffD1) 1)
@@ -87,7 +87,7 @@
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(Asm_simp_tac 1)
+        (asm_simp_tac Lift0_ss 1)
 	]);
 
 (* ------------------------------------------------------------------------ *)
diff -r 42ccfd3e1fb4 -r caef3601c0b2 src/HOLCF/Lift3.ML
--- a/src/HOLCF/Lift3.ML	Mon Oct 09 14:57:55 1995 +0100
+++ b/src/HOLCF/Lift3.ML	Tue Oct 10 11:55:45 1995 +0100
@@ -44,7 +44,7 @@
 	(atac 1),
 	(rtac (monofun_Ilift2 RS ch2ch_monofun) 1),
 	(etac (monofun_Iup RS ch2ch_monofun) 1),
-	(Asm_simp_tac 1)
+        (asm_simp_tac Lift0_ss 1)
 	]);
 
 qed_goal "cont_Iup" Lift3.thy "cont(Iup)"
@@ -70,9 +70,9 @@
 	(etac (monofun_Ilift1 RS ch2ch_monofun) 2),
 	(rtac ext 1),
 	(res_inst_tac [("p","x")] liftE 1),
-	(Asm_simp_tac 1),
+        (asm_simp_tac Lift0_ss 1),
 	(rtac (lub_const RS thelubI RS sym) 1),
-	(Asm_simp_tac 1),
+        (asm_simp_tac Lift0_ss 1),
 	(etac contlub_cfun_fun 1)
 	]);
 
@@ -86,16 +86,16 @@
 	(rtac (thelub_lift1a RS ssubst) 2),
 	(atac 2),
 	(atac 2),
-	(Asm_simp_tac 2),
+        (asm_simp_tac Lift0_ss 2),
 	(rtac (thelub_lift1b RS ssubst) 3),
 	(atac 3),
 	(atac 3),
 	(fast_tac HOL_cs 1),
-	(Asm_simp_tac 2),
+        (asm_simp_tac Lift0_ss 2),
 	(rtac (chain_UU_I_inverse RS sym) 2),
 	(rtac allI 2),
 	(res_inst_tac [("p","Y(i)")] liftE 2),
-	(Asm_simp_tac 2),
+        (asm_simp_tac Lift0_ss 2),
 	(rtac notE 2),
 	(dtac spec 2),
 	(etac spec 2),
@@ -117,7 +117,7 @@
 	(rtac exI 1),
 	(strip_tac 1),
 	(res_inst_tac [("p","Y(i)")] liftE 1),
-	(Asm_simp_tac 2),
+        (asm_simp_tac Lift0_ss 2),
 	(res_inst_tac [("P","Y(i) = UU")] notE 1),
 	(fast_tac HOL_cs 1),
 	(rtac (inst_lift_pcpo RS ssubst) 1),
@@ -148,7 +148,7 @@
 qed_goalw "Exh_Lift1" Lift3.thy [up_def] "z = UU | (? x. z = up`x)"
  (fn prems =>
 	[
-	(simp_tac (!simpset addsimps [cont_Iup]) 1),
+        (simp_tac (Lift0_ss addsimps [cont_Iup]) 1),
 	(rtac (inst_lift_pcpo RS ssubst) 1),
 	(rtac Exh_Lift 1)
 	]);
@@ -159,14 +159,14 @@
 	(cut_facts_tac prems 1),
 	(rtac inject_Iup 1),
 	(etac box_equals 1),
-	(simp_tac (!simpset addsimps [cont_Iup]) 1),
-	(simp_tac (!simpset addsimps [cont_Iup]) 1)
-	]);
+        (simp_tac (Lift0_ss addsimps [cont_Iup]) 1),
+        (simp_tac (Lift0_ss addsimps [cont_Iup]) 1)
+ 	]);
 
 qed_goalw "defined_up" Lift3.thy [up_def] " up`x ~= UU"
  (fn prems =>
 	[
-	(simp_tac (!simpset addsimps [cont_Iup]) 1),
+        (simp_tac (Lift0_ss addsimps [cont_Iup]) 1),
 	(rtac defined_Iup2 1)
 	]);
 
@@ -178,7 +178,7 @@
 	(resolve_tac prems 1),
 	(etac (inst_lift_pcpo RS ssubst) 1),
 	(resolve_tac (tl prems) 1),
-	(asm_simp_tac (!simpset addsimps [cont_Iup]) 1)
+        (asm_simp_tac (Lift0_ss addsimps [cont_Iup]) 1)
 	]);
 
 
@@ -192,7 +192,7 @@
 	(rtac (beta_cfun RS ssubst) 1),
 	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
 		cont_Ilift2,cont2cont_CF1L]) 1)),
-	(simp_tac (!simpset addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
+	(simp_tac (Lift0_ss addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
 	]);
 
 qed_goalw "lift2" Lift3.thy [up_def,lift_def] "lift`f`(up`x)=f`x"
@@ -205,13 +205,13 @@
 		cont_Ilift2,cont2cont_CF1L]) 1)),
 	(rtac (beta_cfun RS ssubst) 1),
 	(rtac cont_Ilift2 1),
-	(simp_tac (!simpset addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
+	(simp_tac (Lift0_ss addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
 	]);
 
 qed_goalw "less_lift4b" Lift3.thy [up_def,lift_def] "~ up`x << UU"
  (fn prems =>
 	[
-	(simp_tac (!simpset addsimps [cont_Iup]) 1),
+        (simp_tac (Lift0_ss addsimps [cont_Iup]) 1),
 	(rtac less_lift3b 1)
 	]);
 
@@ -219,7 +219,7 @@
 	 "(up`x << up`y) = (x<<y)"
  (fn prems =>
 	[
-	(simp_tac (!simpset addsimps [cont_Iup]) 1),
+        (simp_tac (Lift0_ss addsimps [cont_Iup]) 1),
 	(rtac less_lift2c 1)
 	]);
 
@@ -247,7 +247,7 @@
 	(rtac exI 1),
 	(etac box_equals 1),
 	(rtac refl 1),
-	(simp_tac (!simpset addsimps [cont_Iup]) 1)
+	(simp_tac (Lift0_ss addsimps [cont_Iup]) 1)
 	]);
 
 
@@ -268,7 +268,7 @@
 	(dtac notnotD 1),
 	(etac box_equals 1),
 	(rtac refl 1),
-	(simp_tac (!simpset addsimps [cont_Iup]) 1)
+        (simp_tac (Lift0_ss addsimps [cont_Iup]) 1)
 	]);
 
 
@@ -338,8 +338,8 @@
  (fn prems =>
 	[
 	(res_inst_tac [("p","x")] liftE1 1),
-	(asm_simp_tac (!simpset addsimps [lift1,lift2]) 1),
-	(asm_simp_tac (!simpset addsimps [lift1,lift2]) 1)
+	(asm_simp_tac ((simpset_of "Cfun3") addsimps [lift1,lift2]) 1),
+	(asm_simp_tac ((simpset_of "Cfun3") addsimps [lift1,lift2]) 1)
 	]);
 
 (* ------------------------------------------------------------------------ *)
diff -r 42ccfd3e1fb4 -r caef3601c0b2 src/HOLCF/Makefile
--- a/src/HOLCF/Makefile	Mon Oct 09 14:57:55 1995 +0100
+++ b/src/HOLCF/Makefile	Tue Oct 10 11:55:45 1995 +0100
@@ -40,8 +40,8 @@
 $(BIN)/HOL:
 	cd ../HOL;  $(MAKE)
 
-EX_THYS = ex/Coind.thy ex/Hoare.thy \
-           ex/Loop.thy ex/Dagstuhl.thy 
+EX_THYS =  ex/Fix2.thy ex/Hoare.thy \
+           ex/Loop.thy  
 
 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
 
@@ -53,5 +53,21 @@
                 	$(COMP) is not poly or sml;;\
 	esac
 
+EXPLICIT_DOMAINS_THYS = explicit_domains/Coind.thy explicit_domains/Dlist.thy \
+			explicit_domains/Dnat2.thy explicit_domains/Stream.thy \
+			explicit_domains/Dagstuhl.thy explicit_domains/Dnat.thy\
+			explicit_domains/Focus_ex.thy explicit_domains/Stream2.thy
+
+EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS)\
+			 $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
+
+test2:	explicit_domains/ROOT.ML  $(BIN)/HOLCF  $(EXPLICIT_DOMAINS_FILES) 
+	case "$(COMP)" in \
+	poly*)	echo 'exit_use"explicit_domains/ROOT.ML"; quit();' | $(COMP) $(BIN)/HOLCF ;;\
+	sml*)	echo 'exit_use"explicit_domains/ROOT.ML"' | $(BIN)/HOLCF;;\
+	*)	echo Bad value for ISABELLECOMP: \
+                	$(COMP) is not poly or sml;;\
+	esac
+
 .PRECIOUS:  $(BIN)/HOL  $(BIN)/HOLCF 
 
diff -r 42ccfd3e1fb4 -r caef3601c0b2 src/HOLCF/Sprod0.ML
--- a/src/HOLCF/Sprod0.ML	Mon Oct 09 14:57:55 1995 +0100
+++ b/src/HOLCF/Sprod0.ML	Tue Oct 10 11:55:45 1995 +0100
@@ -340,8 +340,10 @@
 (* instantiate the simplifier                                               *)
 (* ------------------------------------------------------------------------ *)
 
-Addsimps [strict_Isfst1,strict_Isfst2,strict_Issnd1,strict_Issnd2,
-	  Isfst2,Issnd2];
+val Sprod0_ss = 
+        HOL_ss 
+        addsimps [strict_Isfst1,strict_Isfst2,strict_Issnd1,strict_Issnd2,
+                 Isfst2,Issnd2];
 
 qed_goal "defined_IsfstIssnd" Sprod0.thy 
 	"p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU"
@@ -352,8 +354,8 @@
 	(contr_tac 1),
 	(hyp_subst_tac 1),
 	(rtac conjI 1),
-	(Asm_simp_tac 1),
-	(Asm_simp_tac 1)
+        (asm_simp_tac Sprod0_ss 1),
+        (asm_simp_tac Sprod0_ss 1)
 	]);
 
 
@@ -366,21 +368,9 @@
 (fn prems =>
 	[
 	(res_inst_tac [("z1","z")] (Exh_Sprod RS disjE) 1),
-	(Asm_simp_tac 1),
+        (asm_simp_tac Sprod0_ss 1),
 	(etac exE 1),
 	(etac exE 1),
-	(Asm_simp_tac 1)
+        (asm_simp_tac Sprod0_ss 1)
 	]);
 
-
-
-
-
-
-
-
-
-
-
-
-
diff -r 42ccfd3e1fb4 -r caef3601c0b2 src/HOLCF/Sprod1.ML
--- a/src/HOLCF/Sprod1.ML	Mon Oct 09 14:57:55 1995 +0100
+++ b/src/HOLCF/Sprod1.ML	Tue Oct 10 11:55:45 1995 +0100
@@ -18,7 +18,7 @@
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(Asm_simp_tac 1)
+        (asm_simp_tac HOL_ss 1)
 	]);
 
 qed_goalw "less_sprod1b" Sprod1.thy [less_sprod_def]
@@ -27,7 +27,7 @@
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(Asm_simp_tac 1)
+        (asm_simp_tac HOL_ss 1)
 	]);
 
 qed_goal "less_sprod2a" Sprod1.thy
@@ -45,7 +45,7 @@
 	(fast_tac HOL_cs 1),
 	(fast_tac HOL_cs 1),
 	(res_inst_tac [("s","Isfst(Ispair UU UU)"),("t","UU")] subst 1),
-	(Simp_tac 1),
+        (simp_tac Sprod0_ss 1),
 	(rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct1) 1),
 	(REPEAT (fast_tac HOL_cs 1))
 	]);
@@ -69,22 +69,22 @@
 	[
 	(rtac conjI 1),
 	(res_inst_tac [("s","Isfst(Ispair xa ya)"),("t","xa")] subst 1),
-	(simp_tac (!simpset addsimps prems)1),
+        (simp_tac (Sprod0_ss addsimps prems)1),
 	(res_inst_tac [("s","Isfst(Ispair x y)"),("t","x")] subst 1),
-	(simp_tac (!simpset addsimps prems)1),
+        (simp_tac (Sprod0_ss addsimps prems)1),
 	(rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct1) 1),
 	(resolve_tac prems 1),
 	(resolve_tac prems 1),
-	(simp_tac (!simpset addsimps prems)1),
+        (simp_tac (Sprod0_ss addsimps prems)1),
 	(res_inst_tac [("s","Issnd(Ispair xa ya)"),("t","ya")] subst 1),
-	(simp_tac (!simpset addsimps prems)1),
-	(res_inst_tac [("s","Issnd(Ispair x y)"),("t","y")] subst 1),
-	(simp_tac (!simpset addsimps prems)1),
-	(rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct2) 1),
+        (simp_tac (Sprod0_ss addsimps prems)1),
+ 	(res_inst_tac [("s","Issnd(Ispair x y)"),("t","y")] subst 1),
+        (simp_tac (Sprod0_ss addsimps prems)1),
+ 	(rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct2) 1),
 	(resolve_tac prems 1),
 	(resolve_tac prems 1),
-	(simp_tac (!simpset addsimps prems)1)
-	]);
+        (simp_tac (Sprod0_ss addsimps prems)1)
+ 	]);
 
 (* ------------------------------------------------------------------------ *)
 (* less_sprod is a partial order on Sprod                                   *)
@@ -123,11 +123,11 @@
 	(hyp_subst_tac 1),
 	(res_inst_tac [("x1","x"),("y1","xa"),("x","y"),("y","ya")] (arg_cong RS cong) 1),
 	(rtac antisym_less 1),
-	(asm_simp_tac (!simpset addsimps [less_sprod2c RS conjunct1]) 1),
-	(asm_simp_tac (!simpset addsimps [less_sprod2c RS conjunct1]) 1),
+        (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct1]) 1),
+        (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct1]) 1),
 	(rtac antisym_less 1),
-	(asm_simp_tac (!simpset addsimps [less_sprod2c RS conjunct2]) 1),
-	(asm_simp_tac (!simpset addsimps [less_sprod2c RS conjunct2]) 1)
+        (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct2]) 1),
+        (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct2]) 1)
 	]);
 
 qed_goal "trans_less_sprod" Sprod1.thy 
diff -r 42ccfd3e1fb4 -r caef3601c0b2 src/HOLCF/Sprod3.ML
--- a/src/HOLCF/Sprod3.ML	Mon Oct 09 14:57:55 1995 +0100
+++ b/src/HOLCF/Sprod3.ML	Tue Oct 10 11:55:45 1995 +0100
@@ -28,7 +28,7 @@
 	(rtac (monofun_Ispair1 RS ch2ch_monofun) 1),
 	(atac 1),
 	(rtac allI 1),
-	(Asm_simp_tac 1),
+        (asm_simp_tac Sprod0_ss 1),
 	(rtac sym 1),
 	(rtac lub_chain_maxelem 1),
 	(res_inst_tac [("P","%j.~Y(j)=UU")] exE 1),
@@ -41,11 +41,13 @@
 	(etac Issnd2 1),
 	(rtac allI 1),
 	(res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1),
-	(Asm_simp_tac 1),
+        (asm_simp_tac Sprod0_ss 1),
+        (rtac refl_less 1),
 	(res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
 	(etac sym 1),
-	(Asm_simp_tac 1)
-	]);
+        (asm_simp_tac Sprod0_ss  1),
+        (rtac minimal 1)
+  	]);
 
 qed_goal "sprod3_lemma2" Sprod3.thy 
 "[| is_chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
@@ -63,7 +65,7 @@
 	(rtac disjI1 1),
 	(rtac chain_UU_I_inverse 1),
 	(rtac allI 1),
-	(Asm_simp_tac  1),
+        (asm_simp_tac Sprod0_ss  1),
 	(etac (chain_UU_I RS spec) 1),
 	(atac 1)
 	]);
@@ -85,7 +87,7 @@
 	(rtac disjI1 1),
 	(rtac chain_UU_I_inverse 1),
 	(rtac allI 1),
-	(Simp_tac  1)
+        (simp_tac Sprod0_ss  1)
 	]);
 
 
@@ -136,17 +138,19 @@
 	(etac Isfst2 1),
 	(rtac allI 1),
 	(res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1),
-	(Asm_simp_tac 1),
-	(res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
+        (asm_simp_tac Sprod0_ss 1),
+        (rtac refl_less 1),
+ 	(res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
 	(etac sym 1),
-	(Asm_simp_tac  1),
+        (asm_simp_tac Sprod0_ss  1),
+        (rtac minimal 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 1)
+        (asm_simp_tac Sprod0_ss 1)
 	]);
 
 qed_goal "sprod3_lemma5" Sprod3.thy 
@@ -165,7 +169,7 @@
 	(rtac disjI2 1),
 	(rtac chain_UU_I_inverse 1),
 	(rtac allI 1),
-	(Asm_simp_tac  1),
+        (asm_simp_tac Sprod0_ss  1),
 	(etac (chain_UU_I RS spec) 1),
 	(atac 1)
 	]);
@@ -186,7 +190,7 @@
 	(rtac disjI1 1),
 	(rtac chain_UU_I_inverse 1),
 	(rtac allI 1),
-	(Simp_tac 1)
+        (simp_tac Sprod0_ss  1)
 	]);
 
 qed_goal "contlub_Ispair2" Sprod3.thy "contlub(Ispair(x))"
@@ -237,12 +241,12 @@
 	(atac 1),
 	(res_inst_tac [("Q","lub(range(%i. Issnd(Y(i))))=UU")]	
 		(excluded_middle RS disjE) 1),
-	(Asm_simp_tac  1),
+        (asm_simp_tac Sprod0_ss  1),
 	(res_inst_tac [("s","UU"),("t","lub(range(%i. Issnd(Y(i))))")]
 		ssubst 1),
 	(atac 1),
 	(rtac trans 1),
-	(Asm_simp_tac  1),
+        (asm_simp_tac Sprod0_ss  1),
 	(rtac sym 1),
 	(rtac chain_UU_I_inverse 1),
 	(rtac allI 1),
@@ -266,11 +270,11 @@
 	(atac 1),
 	(res_inst_tac [("Q","lub(range(%i. Isfst(Y(i))))=UU")]
 	 (excluded_middle RS disjE) 1),
-	(Asm_simp_tac  1),
+        (asm_simp_tac Sprod0_ss  1),
 	(res_inst_tac [("s","UU"),("t","lub(range(%i. Isfst(Y(i))))")] 
 		ssubst 1),
 	(atac 1),
-	(Asm_simp_tac  1),
+        (asm_simp_tac Sprod0_ss  1),
 	(rtac sym 1),
 	(rtac chain_UU_I_inverse 1),
 	(rtac allI 1),
@@ -680,5 +684,5 @@
 		ssplit1,ssplit2];
 
 Addsimps [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2,
-	  strict_ssnd1,strict_ssnd2,sfst2,ssnd2,
+	  strict_ssnd1,strict_ssnd2,sfst2,ssnd2,defined_spair,
 	  ssplit1,ssplit2];
diff -r 42ccfd3e1fb4 -r caef3601c0b2 src/HOLCF/Ssum0.ML
--- a/src/HOLCF/Ssum0.ML	Mon Oct 09 14:57:55 1995 +0100
+++ b/src/HOLCF/Ssum0.ML	Tue Oct 10 11:55:45 1995 +0100
@@ -388,4 +388,6 @@
 (* instantiate the simplifier                                               *)
 (* ------------------------------------------------------------------------ *)
 
-Addsimps [(strict_IsinlIsinr RS sym),Iwhen1,Iwhen2,Iwhen3];
+val Ssum0_ss = (simpset_of "Cfun3") addsimps 
+                [(strict_IsinlIsinr RS sym),Iwhen1,Iwhen2,Iwhen3];
+
diff -r 42ccfd3e1fb4 -r caef3601c0b2 src/HOLCF/Ssum2.ML
--- a/src/HOLCF/Ssum2.ML	Mon Oct 09 14:57:55 1995 +0100
+++ b/src/HOLCF/Ssum2.ML	Tue Oct 10 11:55:45 1995 +0100
@@ -97,11 +97,11 @@
 	(strip_tac 1),
 	(res_inst_tac [("p","xb")] IssumE 1),
 	(hyp_subst_tac 1),
-	(Asm_simp_tac 1),
-	(Asm_simp_tac 1),
-	(etac monofun_cfun_fun 1),
-	(Asm_simp_tac 1)
-	]);
+        (asm_simp_tac Ssum0_ss 1),
+        (asm_simp_tac Ssum0_ss 1),
+        (etac monofun_cfun_fun 1),
+        (asm_simp_tac Ssum0_ss 1)
+ 	]);
 
 qed_goalw "monofun_Iwhen2" Ssum2.thy [monofun] "monofun(Iwhen(f))"
  (fn prems =>
@@ -111,9 +111,9 @@
 	(strip_tac 1),
 	(res_inst_tac [("p","xa")] IssumE 1),
 	(hyp_subst_tac 1),
-	(Asm_simp_tac 1),
-	(Asm_simp_tac 1),
-	(Asm_simp_tac 1),
+        (asm_simp_tac Ssum0_ss 1),
+        (asm_simp_tac Ssum0_ss 1),
+        (asm_simp_tac Ssum0_ss 1),
 	(etac monofun_cfun_fun 1)
 	]);
 
@@ -123,36 +123,36 @@
 	(strip_tac 1),
 	(res_inst_tac [("p","x")] IssumE 1),
 	(hyp_subst_tac 1),
-	(Asm_simp_tac 1),
+        (asm_simp_tac Ssum0_ss 1),
 	(hyp_subst_tac 1),
 	(res_inst_tac [("p","y")] IssumE 1),
 	(hyp_subst_tac 1),
-	(Asm_simp_tac 1),
+        (asm_simp_tac Ssum0_ss 1),
 	(res_inst_tac  [("P","xa=UU")] notE 1),
 	(atac 1),
 	(rtac UU_I 1),
 	(rtac (less_ssum3a  RS iffD1) 1),
 	(atac 1),
 	(hyp_subst_tac 1),
-	(Asm_simp_tac 1),
+        (asm_simp_tac Ssum0_ss 1),
 	(rtac monofun_cfun_arg 1),
 	(etac (less_ssum3a  RS iffD1) 1),
 	(hyp_subst_tac 1),
 	(res_inst_tac [("s","UU"),("t","xa")] subst 1),
 	(etac (less_ssum3c  RS iffD1 RS sym) 1),
-	(Asm_simp_tac 1),
+        (asm_simp_tac Ssum0_ss 1),
 	(hyp_subst_tac 1),
 	(res_inst_tac [("p","y")] IssumE 1),
 	(hyp_subst_tac 1),
 	(res_inst_tac [("s","UU"),("t","ya")] subst 1),
 	(etac (less_ssum3d  RS iffD1 RS sym) 1),
-	(Asm_simp_tac 1),
+        (asm_simp_tac Ssum0_ss 1),
 	(hyp_subst_tac 1),
 	(res_inst_tac [("s","UU"),("t","ya")] subst 1),
 	(etac (less_ssum3d  RS iffD1 RS sym) 1),
-	(Asm_simp_tac 1),
+        (asm_simp_tac Ssum0_ss 1),
 	(hyp_subst_tac 1),
-	(Asm_simp_tac 1),
+        (asm_simp_tac Ssum0_ss 1),
 	(rtac monofun_cfun_arg 1),
 	(etac (less_ssum3b  RS iffD1) 1)
 	]);
@@ -247,8 +247,8 @@
 	(cut_facts_tac prems 1),
 	(hyp_subst_tac 1),
 	(res_inst_tac [("Q","x=UU")] classical2 1),
-	(Asm_simp_tac 1),
-	(Asm_simp_tac 1)
+        (asm_simp_tac Ssum0_ss 1),
+        (asm_simp_tac Ssum0_ss 1)
 	]);
 
 (* ------------------------------------------------------------------------ *)
@@ -262,8 +262,8 @@
 	(cut_facts_tac prems 1),
 	(hyp_subst_tac 1),
 	(res_inst_tac [("Q","x=UU")] classical2 1),
-	(Asm_simp_tac 1),
-	(Asm_simp_tac 1)
+        (asm_simp_tac Ssum0_ss 1),
+        (asm_simp_tac Ssum0_ss 1)
 	]);
 
 (* ------------------------------------------------------------------------ *)
@@ -339,8 +339,8 @@
 	(rtac chain_UU_I_inverse 1),
 	(rtac allI 1),
 	(res_inst_tac [("p","Y(i)")] IssumE 1),
-	(Asm_simp_tac 1),
-	(Asm_simp_tac 2),
+	(asm_simp_tac Ssum0_ss 1),
+	(asm_simp_tac Ssum0_ss 2),
 	(etac notE 1),
 	(rtac (less_ssum3c RS iffD1) 1),
 	(res_inst_tac [("t","Isinl(x)")] subst 1),
@@ -374,9 +374,9 @@
 	(rtac chain_UU_I_inverse 1),
 	(rtac allI 1),
 	(res_inst_tac [("p","Y(i)")] IssumE 1),
-	(Asm_simp_tac 1),
-	(Asm_simp_tac 1),
-	(etac notE 1),
+	(asm_simp_tac Ssum0_ss 1),
+	(asm_simp_tac Ssum0_ss 1),
+ 	(etac notE 1),
 	(rtac (less_ssum3d RS iffD1) 1),
 	(res_inst_tac [("t","Isinr(y)")] subst 1),
 	(atac 1),
diff -r 42ccfd3e1fb4 -r caef3601c0b2 src/HOLCF/Ssum3.ML
--- a/src/HOLCF/Ssum3.ML	Mon Oct 09 14:57:55 1995 +0100
+++ b/src/HOLCF/Ssum3.ML	Tue Oct 10 11:55:45 1995 +0100
@@ -41,9 +41,9 @@
 	(etac (monofun_Isinl RS ch2ch_monofun) 1),
 	(rtac allI 1),
 	(res_inst_tac [("Q","Y(k)=UU")] classical2 1),
-	(Asm_simp_tac 1),
-	(Asm_simp_tac 1)
-	]);
+	(asm_simp_tac Ssum0_ss 1),
+	(asm_simp_tac Ssum0_ss 1)
+ 	]);
 
 qed_goal "contlub_Isinr" Ssum3.thy "contlub(Isinr)"
  (fn prems =>
@@ -72,8 +72,8 @@
 	(etac (monofun_Isinr RS ch2ch_monofun) 1),
 	(rtac allI 1),
 	(res_inst_tac [("Q","Y(k)=UU")] classical2 1),
-	(Asm_simp_tac 1),
-	(Asm_simp_tac 1)
+	(asm_simp_tac Ssum0_ss 1),
+	(asm_simp_tac Ssum0_ss 1)
 	]);
 
 qed_goal "cont_Isinl" Ssum3.thy "cont(Isinl)"
@@ -114,11 +114,11 @@
 	(rtac (expand_fun_eq RS iffD2) 1),
 	(strip_tac 1),
 	(res_inst_tac [("p","xa")] IssumE 1),
-	(Asm_simp_tac 1),
+	(asm_simp_tac Ssum0_ss 1),
 	(rtac (lub_const RS thelubI RS sym) 1),
-	(Asm_simp_tac 1),
+	(asm_simp_tac Ssum0_ss 1),
 	(etac contlub_cfun_fun 1),
-	(Asm_simp_tac 1),
+	(asm_simp_tac Ssum0_ss 1),
 	(rtac (lub_const RS thelubI RS sym) 1)
 	]);
 
@@ -133,11 +133,11 @@
 	(rtac (expand_fun_eq RS iffD2) 1),
 	(strip_tac 1),
 	(res_inst_tac [("p","x")] IssumE 1),
-	(Asm_simp_tac 1),
+	(asm_simp_tac Ssum0_ss 1),
 	(rtac (lub_const RS thelubI RS sym) 1),
-	(Asm_simp_tac 1),
+	(asm_simp_tac Ssum0_ss 1),
 	(rtac (lub_const RS thelubI RS sym) 1),
-	(Asm_simp_tac 1),
+	(asm_simp_tac Ssum0_ss 1),
 	(etac contlub_cfun_fun 1)
 	]);
 
@@ -192,7 +192,7 @@
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(Asm_simp_tac 1),
+	(asm_simp_tac Ssum0_ss 1),
 	(rtac (chain_UU_I_inverse RS sym) 1),
 	(rtac allI 1),
 	(res_inst_tac [("s","Isinl(UU)"),("t","Y(i)")] subst 1),
@@ -200,7 +200,7 @@
 	(rtac (chain_UU_I RS spec RS sym) 1),
 	(atac 1),
 	(etac (inst_ssum_pcpo RS ssubst) 1),
-	(Asm_simp_tac 1)
+	(asm_simp_tac Ssum0_ss 1)
 	]);
 
 qed_goal "ssum_lemma12" Ssum3.thy 
@@ -209,7 +209,7 @@
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(Asm_simp_tac 1),
+	(asm_simp_tac Ssum0_ss 1),
 	(res_inst_tac [("t","x")] subst 1),
 	(rtac inject_Isinl 1),
 	(rtac trans 1),
@@ -255,7 +255,7 @@
 	(res_inst_tac [("t","Y(i)")] ssubst 1),
 	(atac 1),
 	(fast_tac HOL_cs 1),
-	(Simp_tac 1),
+        (simp_tac (simpset_of "Cfun3") 1),
 	(rtac (monofun_fapp2 RS ch2ch_monofun) 1),
 	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
 	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
@@ -268,7 +268,7 @@
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(Asm_simp_tac 1),
+	(asm_simp_tac Ssum0_ss 1),
 	(res_inst_tac [("t","x")] subst 1),
 	(rtac inject_Isinr 1),
 	(rtac trans 1),
@@ -319,7 +319,7 @@
 	(res_inst_tac [("t","Y(i)")] ssubst 1),
 	(atac 1),
 	(fast_tac HOL_cs 1),
-	(Simp_tac 1),
+        (simp_tac (simpset_of "Cfun3") 1),
 	(rtac (monofun_fapp2 RS ch2ch_monofun) 1),
 	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
 	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
@@ -373,14 +373,14 @@
 qed_goalw "strict_sinl" Ssum3.thy [sinl_def] "sinl`UU =UU"
  (fn prems =>
 	[
-	(simp_tac (!simpset addsimps [cont_Isinl]) 1),
+	(simp_tac (Ssum0_ss 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 (!simpset addsimps [cont_Isinr]) 1),
+	(simp_tac (Ssum0_ss addsimps [cont_Isinr]) 1),
 	(rtac (inst_ssum_pcpo RS sym) 1)
 	]);
 
@@ -391,8 +391,8 @@
 	(cut_facts_tac prems 1),
 	(rtac noteq_IsinlIsinr 1),
 	(etac box_equals 1),
-	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
-	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1)
+	(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1),
+	(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1)
 	]);
 
 qed_goalw "inject_sinl" Ssum3.thy [sinl_def,sinr_def] 
@@ -402,8 +402,8 @@
 	(cut_facts_tac prems 1),
 	(rtac inject_Isinl 1),
 	(etac box_equals 1),
-	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
-	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1)
+	(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1),
+	(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1)
 	]);
 
 qed_goalw "inject_sinr" Ssum3.thy [sinl_def,sinr_def] 
@@ -413,8 +413,8 @@
 	(cut_facts_tac prems 1),
 	(rtac inject_Isinr 1),
 	(etac box_equals 1),
-	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
-	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1)
+	(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1),
+	(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1)
 	]);
 
 
@@ -444,7 +444,7 @@
 	"z=UU | (? a. z=sinl`a & a~=UU) | (? b. z=sinr`b & b~=UU)"
  (fn prems =>
 	[
-	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
+	(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1),
 	(rtac (inst_ssum_pcpo RS ssubst) 1),
 	(rtac Exh_Ssum 1)
 	]);
@@ -462,11 +462,11 @@
 	(atac 1),
 	(resolve_tac prems 1),
 	(atac 2),
-	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
+	(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1),
 	(resolve_tac prems 1),
 	(atac 2),
-	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1)
-	]);
+	(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1)
+ 	]);
 
 
 qed_goalw "ssumE2" Ssum3.thy [sinl_def,sinr_def] 
@@ -499,7 +499,7 @@
 	(rtac (beta_cfun RS ssubst) 1),
 	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
 		cont_Iwhen3,cont2cont_CF1L]) 1)),
-	(Simp_tac 1)
+	(simp_tac Ssum0_ss  1)
 	]);
 
 qed_goalw "sswhen2" Ssum3.thy [sswhen_def,sinl_def,sinr_def] 
@@ -519,7 +519,7 @@
 	(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  1)
+	(asm_simp_tac Ssum0_ss  1)
 	]);
 
 
@@ -541,8 +541,8 @@
 	(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 1)
-	]);
+	(asm_simp_tac Ssum0_ss  1)
+ 	]);
 
 
 qed_goalw "less_ssum4a" Ssum3.thy [sinl_def,sinr_def] 
@@ -602,7 +602,7 @@
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
+	(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1),
 	(etac ssum_lemma4 1)
 	]);
 
@@ -629,7 +629,7 @@
 	(rtac exI 1),
 	(etac box_equals 1),
 	(rtac refl 1),
-	(asm_simp_tac (!simpset addsimps [cont_Isinl]) 1)
+	(asm_simp_tac (Ssum0_ss addsimps [cont_Isinl]) 1)
 	]);
 
 qed_goalw "thelub_ssum2b" Ssum3.thy [sinl_def,sinr_def,sswhen_def] 
@@ -658,7 +658,7 @@
 	(rtac exI 1),
 	(etac box_equals 1),
 	(rtac refl 1),
-	(asm_simp_tac (!simpset addsimps 
+	(asm_simp_tac (Ssum0_ss addsimps 
 	[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
 	cont_Iwhen3]) 1)
 	]);
@@ -668,11 +668,11 @@
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(asm_simp_tac (!simpset addsimps 
+	(asm_simp_tac (Ssum0_ss addsimps 
 	[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
 	cont_Iwhen3]) 1),
 	(etac ssum_lemma9 1),
-	(asm_simp_tac (!simpset addsimps 
+	(asm_simp_tac (Ssum0_ss addsimps 
 	[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
 	cont_Iwhen3]) 1)
 	]);
@@ -682,11 +682,11 @@
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(asm_simp_tac (!simpset addsimps 
+	(asm_simp_tac (Ssum0_ss addsimps 
 	[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
 	cont_Iwhen3]) 1),
 	(etac ssum_lemma10 1),
-	(asm_simp_tac (!simpset addsimps 
+	(asm_simp_tac (Ssum0_ss addsimps 
 	[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
 	cont_Iwhen3]) 1)
 	]);
@@ -714,9 +714,9 @@
  (fn prems =>
 	[
 	(res_inst_tac [("p","z")] ssumE 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)
+        (asm_simp_tac ((simpset_of "Cfun3") addsimps [sswhen1,sswhen2,sswhen3]) 1),
+        (asm_simp_tac ((simpset_of "Cfun3") addsimps [sswhen1,sswhen2,sswhen3]) 1),
+        (asm_simp_tac ((simpset_of "Cfun3") addsimps [sswhen1,sswhen2,sswhen3]) 1)
 	]);