diff -r 7edd3e5f26d4 -r 428385c4bc50 src/HOLCF/Ssum0.ML
--- a/src/HOLCF/Ssum0.ML	Tue Jul 04 14:58:40 2000 +0200
+++ b/src/HOLCF/Ssum0.ML	Tue Jul 04 15:58:11 2000 +0200
@@ -10,23 +10,19 @@
 (* A non-emptyness result for Sssum                                         *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "SsumIl" Ssum0.thy [Ssum_def] "Sinl_Rep(a):Ssum"
- (fn prems =>
-        [
-        (rtac CollectI 1),
-        (rtac disjI1 1),
-        (rtac exI 1),
-        (rtac refl 1)
-        ]);
+val prems = goalw Ssum0.thy [Ssum_def] "Sinl_Rep(a):Ssum";
+by (rtac CollectI 1);
+by (rtac disjI1 1);
+by (rtac exI 1);
+by (rtac refl 1);
+qed "SsumIl";
 
-qed_goalw "SsumIr" Ssum0.thy [Ssum_def] "Sinr_Rep(a):Ssum"
- (fn prems =>
-        [
-        (rtac CollectI 1),
-        (rtac disjI2 1),
-        (rtac exI 1),
-        (rtac refl 1)
-        ]);
+val prems = goalw Ssum0.thy [Ssum_def] "Sinr_Rep(a):Ssum";
+by (rtac CollectI 1);
+by (rtac disjI2 1);
+by (rtac exI 1);
+by (rtac refl 1);
+qed "SsumIr";
 
 Goal "inj_on Abs_Ssum Ssum";
 by (rtac inj_on_inverseI 1);
@@ -37,58 +33,48 @@
 (* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr                        *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "strict_SinlSinr_Rep" Ssum0.thy [Sinr_Rep_def,Sinl_Rep_def]
- "Sinl_Rep(UU) = Sinr_Rep(UU)"
- (fn prems =>
-        [
-        (rtac ext 1),
-        (rtac ext 1),
-        (rtac ext 1),
-        (fast_tac HOL_cs 1)
-        ]);
+val prems = goalw Ssum0.thy [Sinr_Rep_def,Sinl_Rep_def]
+ "Sinl_Rep(UU) = Sinr_Rep(UU)";
+by (rtac ext 1);
+by (rtac ext 1);
+by (rtac ext 1);
+by (fast_tac HOL_cs 1);
+qed "strict_SinlSinr_Rep";
 
-qed_goalw "strict_IsinlIsinr" Ssum0.thy [Isinl_def,Isinr_def]
- "Isinl(UU) = Isinr(UU)"
- (fn prems =>
-        [
-        (rtac (strict_SinlSinr_Rep RS arg_cong) 1)
-        ]);
+val prems = goalw Ssum0.thy [Isinl_def,Isinr_def]
+ "Isinl(UU) = Isinr(UU)";
+by (rtac (strict_SinlSinr_Rep RS arg_cong) 1);
+qed "strict_IsinlIsinr";
 
 
 (* ------------------------------------------------------------------------ *)
 (* distinctness of  Sinl_Rep, Sinr_Rep and Isinl, Isinr                     *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "noteq_SinlSinr_Rep" Ssum0.thy [Sinl_Rep_def,Sinr_Rep_def]
-        "(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU"
- (fn prems =>
-        [
-        (rtac conjI 1),
-        (case_tac "a=UU" 1),
-        (atac 1),
-        (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD2 
-        RS mp RS conjunct1 RS sym) 1),
-        (fast_tac HOL_cs 1),
-        (atac 1),
-        (case_tac "b=UU" 1),
-        (atac 1),
-        (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD1 
-        RS mp RS conjunct1 RS sym) 1),
-        (fast_tac HOL_cs 1),
-        (atac 1)
-        ]);
+val prems = goalw Ssum0.thy [Sinl_Rep_def,Sinr_Rep_def]
+        "(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU";
+by (rtac conjI 1);
+by (case_tac "a=UU" 1);
+by (atac 1);
+by (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD2  RS mp RS conjunct1 RS sym) 1);
+by (fast_tac HOL_cs 1);
+by (atac 1);
+by (case_tac "b=UU" 1);
+by (atac 1);
+by (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD1  RS mp RS conjunct1 RS sym) 1);
+by (fast_tac HOL_cs 1);
+by (atac 1);
+qed "noteq_SinlSinr_Rep";
 
 
-qed_goalw "noteq_IsinlIsinr" Ssum0.thy [Isinl_def,Isinr_def]
-        "Isinl(a)=Isinr(b) ==> a=UU & b=UU"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac noteq_SinlSinr_Rep 1),
-        (etac (inj_on_Abs_Ssum  RS inj_onD) 1),
-        (rtac SsumIl 1),
-        (rtac SsumIr 1)
-        ]);
+val prems = goalw Ssum0.thy [Isinl_def,Isinr_def]
+        "Isinl(a)=Isinr(b) ==> a=UU & b=UU";
+by (cut_facts_tac prems 1);
+by (rtac noteq_SinlSinr_Rep 1);
+by (etac (inj_on_Abs_Ssum  RS inj_onD) 1);
+by (rtac SsumIl 1);
+by (rtac SsumIr 1);
+qed "noteq_IsinlIsinr";
 
 
 
@@ -96,49 +82,37 @@
 (* injectivity of Sinl_Rep, Sinr_Rep and Isinl, Isinr                       *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "inject_Sinl_Rep1" Ssum0.thy [Sinl_Rep_def]
- "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU"
- (fn prems =>
-        [
-        (case_tac "a=UU" 1),
-        (atac 1),
-        (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong 
-        RS iffD2 RS mp RS conjunct1 RS sym) 1),
-        (fast_tac HOL_cs 1),
-        (atac 1)
-        ]);
+val prems = goalw Ssum0.thy [Sinl_Rep_def]
+ "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU";
+by (case_tac "a=UU" 1);
+by (atac 1);
+by (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong  RS iffD2 RS mp RS conjunct1 RS sym) 1);
+by (fast_tac HOL_cs 1);
+by (atac 1);
+qed "inject_Sinl_Rep1";
 
-qed_goalw "inject_Sinr_Rep1" Ssum0.thy [Sinr_Rep_def]
- "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU"
- (fn prems =>
-        [
-        (case_tac "b=UU" 1),
-        (atac 1),
-        (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong 
-        RS iffD2 RS mp RS conjunct1 RS sym) 1),
-        (fast_tac HOL_cs 1),
-        (atac 1)
-        ]);
+val prems = goalw Ssum0.thy [Sinr_Rep_def]
+ "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU";
+by (case_tac "b=UU" 1);
+by (atac 1);
+by (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong  RS iffD2 RS mp RS conjunct1 RS sym) 1);
+by (fast_tac HOL_cs 1);
+by (atac 1);
+qed "inject_Sinr_Rep1";
 
-qed_goalw "inject_Sinl_Rep2" Ssum0.thy [Sinl_Rep_def]
-"[| a1~=UU ; a2~=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2"
- (fn prems =>
-        [
-        (rtac ((nth_elem (2,prems)) RS fun_cong  RS fun_cong RS fun_cong 
-        RS iffD1 RS mp RS conjunct1) 1),
-        (fast_tac HOL_cs 1),
-        (resolve_tac prems 1)
-        ]);
+val prems = goalw Ssum0.thy [Sinl_Rep_def]
+"[| a1~=UU ; a2~=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2";
+by (rtac ((nth_elem (2,prems)) RS fun_cong  RS fun_cong RS fun_cong  RS iffD1 RS mp RS conjunct1) 1);
+by (fast_tac HOL_cs 1);
+by (resolve_tac prems 1);
+qed "inject_Sinl_Rep2";
 
-qed_goalw "inject_Sinr_Rep2" Ssum0.thy [Sinr_Rep_def]
-"[|b1~=UU ; b2~=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2"
- (fn prems =>
-        [
-        (rtac ((nth_elem (2,prems)) RS fun_cong  RS fun_cong RS fun_cong 
-        RS iffD1 RS mp RS conjunct1) 1),
-        (fast_tac HOL_cs 1),
-        (resolve_tac prems 1)
-        ]);
+val prems = goalw Ssum0.thy [Sinr_Rep_def]
+"[|b1~=UU ; b2~=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2";
+by (rtac ((nth_elem (2,prems)) RS fun_cong  RS fun_cong RS fun_cong  RS iffD1 RS mp RS conjunct1) 1);
+by (fast_tac HOL_cs 1);
+by (resolve_tac prems 1);
+qed "inject_Sinr_Rep2";
 
 Goal "Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2";
 by (case_tac "a1=UU" 1);
@@ -166,27 +140,23 @@
 by (atac 1);
 qed "inject_Sinr_Rep";
 
-qed_goalw "inject_Isinl" Ssum0.thy [Isinl_def]
-"Isinl(a1)=Isinl(a2)==> a1=a2"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac inject_Sinl_Rep 1),
-        (etac (inj_on_Abs_Ssum  RS inj_onD) 1),
-        (rtac SsumIl 1),
-        (rtac SsumIl 1)
-        ]);
+val prems = goalw Ssum0.thy [Isinl_def]
+"Isinl(a1)=Isinl(a2)==> a1=a2";
+by (cut_facts_tac prems 1);
+by (rtac inject_Sinl_Rep 1);
+by (etac (inj_on_Abs_Ssum  RS inj_onD) 1);
+by (rtac SsumIl 1);
+by (rtac SsumIl 1);
+qed "inject_Isinl";
 
-qed_goalw "inject_Isinr" Ssum0.thy [Isinr_def]
-"Isinr(b1)=Isinr(b2) ==> b1=b2"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac inject_Sinr_Rep 1),
-        (etac (inj_on_Abs_Ssum  RS inj_onD) 1),
-        (rtac SsumIr 1),
-        (rtac SsumIr 1)
-        ]);
+val prems = goalw Ssum0.thy [Isinr_def]
+"Isinr(b1)=Isinr(b2) ==> b1=b2";
+by (cut_facts_tac prems 1);
+by (rtac inject_Sinr_Rep 1);
+by (etac (inj_on_Abs_Ssum  RS inj_onD) 1);
+by (rtac SsumIr 1);
+by (rtac SsumIr 1);
+qed "inject_Isinr";
 
 Goal "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)";
 by (rtac contrapos 1);
@@ -205,46 +175,44 @@
 (* choice of the bottom representation is arbitrary                         *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "Exh_Ssum" Ssum0.thy [Isinl_def,Isinr_def]
-        "z=Isinl(UU) | (? a. z=Isinl(a) & a~=UU) | (? b. z=Isinr(b) & b~=UU)"
- (fn prems =>
-        [
-        (rtac (rewrite_rule [Ssum_def] Rep_Ssum RS CollectE) 1),
-        (etac disjE 1),
-        (etac exE 1),
-        (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1),
-        (etac disjI1 1),
-        (rtac disjI2 1),
-        (rtac disjI1 1),
-        (rtac exI 1),
-        (rtac conjI 1),
-        (rtac (Rep_Ssum_inverse RS sym RS trans) 1),
-        (etac arg_cong 1),
-        (res_inst_tac [("Q","Sinl_Rep(a)=Sinl_Rep(UU)")] contrapos 1),
-        (etac arg_cong 2),
-        (etac contrapos 1),
-        (rtac (Rep_Ssum_inverse RS sym RS trans) 1),
-        (rtac trans 1),
-        (etac arg_cong 1),
-        (etac arg_cong 1),
-        (etac exE 1),
-        (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1),
-        (etac disjI1 1),
-        (rtac disjI2 1),
-        (rtac disjI2 1),
-        (rtac exI 1),
-        (rtac conjI 1),
-        (rtac (Rep_Ssum_inverse RS sym RS trans) 1),
-        (etac arg_cong 1),
-        (res_inst_tac [("Q","Sinr_Rep(b)=Sinl_Rep(UU)")] contrapos 1),
-        (hyp_subst_tac 2),
-        (rtac (strict_SinlSinr_Rep RS sym) 2),
-        (etac contrapos 1),
-        (rtac (Rep_Ssum_inverse RS sym RS trans) 1),
-        (rtac trans 1),
-        (etac arg_cong 1),
-        (etac arg_cong 1)
-        ]);
+val prems = goalw Ssum0.thy [Isinl_def,Isinr_def]
+        "z=Isinl(UU) | (? a. z=Isinl(a) & a~=UU) | (? b. z=Isinr(b) & b~=UU)";
+by (rtac (rewrite_rule [Ssum_def] Rep_Ssum RS CollectE) 1);
+by (etac disjE 1);
+by (etac exE 1);
+by (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1);
+by (etac disjI1 1);
+by (rtac disjI2 1);
+by (rtac disjI1 1);
+by (rtac exI 1);
+by (rtac conjI 1);
+by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
+by (etac arg_cong 1);
+by (res_inst_tac [("Q","Sinl_Rep(a)=Sinl_Rep(UU)")] contrapos 1);
+by (etac arg_cong 2);
+by (etac contrapos 1);
+by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
+by (rtac trans 1);
+by (etac arg_cong 1);
+by (etac arg_cong 1);
+by (etac exE 1);
+by (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1);
+by (etac disjI1 1);
+by (rtac disjI2 1);
+by (rtac disjI2 1);
+by (rtac exI 1);
+by (rtac conjI 1);
+by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
+by (etac arg_cong 1);
+by (res_inst_tac [("Q","Sinr_Rep(b)=Sinl_Rep(UU)")] contrapos 1);
+by (hyp_subst_tac 2);
+by (rtac (strict_SinlSinr_Rep RS sym) 2);
+by (etac contrapos 1);
+by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
+by (rtac trans 1);
+by (etac arg_cong 1);
+by (etac arg_cong 1);
+qed "Exh_Ssum";
 
 (* ------------------------------------------------------------------------ *)
 (* elimination rules for the strict sum ++                                  *)
@@ -282,83 +250,77 @@
 (* rewrites for Iwhen                                                       *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "Iwhen1" Ssum0.thy [Iwhen_def]
-        "Iwhen f g (Isinl UU) = UU"
- (fn prems =>
-        [
-        (rtac select_equality 1),
-        (rtac conjI 1),
-        (fast_tac HOL_cs  1),
-        (rtac conjI 1),
-        (strip_tac 1),
-        (res_inst_tac [("P","a=UU")] notE 1),
-        (fast_tac HOL_cs  1),
-        (rtac inject_Isinl 1),
-        (rtac sym 1),
-        (fast_tac HOL_cs  1),
-        (strip_tac 1),
-        (res_inst_tac [("P","b=UU")] notE 1),
-        (fast_tac HOL_cs  1),
-        (rtac inject_Isinr 1),
-        (rtac sym 1),
-        (rtac (strict_IsinlIsinr RS subst) 1),
-        (fast_tac HOL_cs  1),
-        (fast_tac HOL_cs  1)
-        ]);
+val prems = goalw Ssum0.thy [Iwhen_def]
+        "Iwhen f g (Isinl UU) = UU";
+by (rtac select_equality 1);
+by (rtac conjI 1);
+by (fast_tac HOL_cs  1);
+by (rtac conjI 1);
+by (strip_tac 1);
+by (res_inst_tac [("P","a=UU")] notE 1);
+by (fast_tac HOL_cs  1);
+by (rtac inject_Isinl 1);
+by (rtac sym 1);
+by (fast_tac HOL_cs  1);
+by (strip_tac 1);
+by (res_inst_tac [("P","b=UU")] notE 1);
+by (fast_tac HOL_cs  1);
+by (rtac inject_Isinr 1);
+by (rtac sym 1);
+by (rtac (strict_IsinlIsinr RS subst) 1);
+by (fast_tac HOL_cs  1);
+by (fast_tac HOL_cs  1);
+qed "Iwhen1";
 
 
-qed_goalw "Iwhen2" Ssum0.thy [Iwhen_def]
-        "x~=UU ==> Iwhen f g (Isinl x) = f`x"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac select_equality 1),
-        (fast_tac HOL_cs  2),
-        (rtac conjI 1),
-        (strip_tac 1),
-        (res_inst_tac [("P","x=UU")] notE 1),
-        (atac 1),
-        (rtac inject_Isinl 1),
-        (atac 1),
-        (rtac conjI 1),
-        (strip_tac 1),
-        (rtac cfun_arg_cong 1),
-        (rtac inject_Isinl 1),
-        (fast_tac HOL_cs  1),
-        (strip_tac 1),
-        (res_inst_tac [("P","Isinl(x) = Isinr(b)")] notE 1),
-        (fast_tac HOL_cs  2),
-        (rtac contrapos 1),
-        (etac noteq_IsinlIsinr 2),
-        (fast_tac HOL_cs  1)
-        ]);
+val prems = goalw Ssum0.thy [Iwhen_def]
+        "x~=UU ==> Iwhen f g (Isinl x) = f`x";
+by (cut_facts_tac prems 1);
+by (rtac select_equality 1);
+by (fast_tac HOL_cs  2);
+by (rtac conjI 1);
+by (strip_tac 1);
+by (res_inst_tac [("P","x=UU")] notE 1);
+by (atac 1);
+by (rtac inject_Isinl 1);
+by (atac 1);
+by (rtac conjI 1);
+by (strip_tac 1);
+by (rtac cfun_arg_cong 1);
+by (rtac inject_Isinl 1);
+by (fast_tac HOL_cs  1);
+by (strip_tac 1);
+by (res_inst_tac [("P","Isinl(x) = Isinr(b)")] notE 1);
+by (fast_tac HOL_cs  2);
+by (rtac contrapos 1);
+by (etac noteq_IsinlIsinr 2);
+by (fast_tac HOL_cs  1);
+qed "Iwhen2";
 
-qed_goalw "Iwhen3" Ssum0.thy [Iwhen_def]
-        "y~=UU ==> Iwhen f g (Isinr y) = g`y"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac select_equality 1),
-        (fast_tac HOL_cs  2),
-        (rtac conjI 1),
-        (strip_tac 1),
-        (res_inst_tac [("P","y=UU")] notE 1),
-        (atac 1),
-        (rtac inject_Isinr 1),
-        (rtac (strict_IsinlIsinr RS subst) 1),
-        (atac 1),
-        (rtac conjI 1),
-        (strip_tac 1),
-        (res_inst_tac [("P","Isinr(y) = Isinl(a)")] notE 1),
-        (fast_tac HOL_cs  2),
-        (rtac contrapos 1),
-        (etac (sym RS noteq_IsinlIsinr) 2),
-        (fast_tac HOL_cs  1),
-        (strip_tac 1),
-        (rtac cfun_arg_cong 1),
-        (rtac inject_Isinr 1),
-        (fast_tac HOL_cs  1)
-        ]);
+val prems = goalw Ssum0.thy [Iwhen_def]
+        "y~=UU ==> Iwhen f g (Isinr y) = g`y";
+by (cut_facts_tac prems 1);
+by (rtac select_equality 1);
+by (fast_tac HOL_cs  2);
+by (rtac conjI 1);
+by (strip_tac 1);
+by (res_inst_tac [("P","y=UU")] notE 1);
+by (atac 1);
+by (rtac inject_Isinr 1);
+by (rtac (strict_IsinlIsinr RS subst) 1);
+by (atac 1);
+by (rtac conjI 1);
+by (strip_tac 1);
+by (res_inst_tac [("P","Isinr(y) = Isinl(a)")] notE 1);
+by (fast_tac HOL_cs  2);
+by (rtac contrapos 1);
+by (etac (sym RS noteq_IsinlIsinr) 2);
+by (fast_tac HOL_cs  1);
+by (strip_tac 1);
+by (rtac cfun_arg_cong 1);
+by (rtac inject_Isinr 1);
+by (fast_tac HOL_cs  1);
+qed "Iwhen3";
 
 (* ------------------------------------------------------------------------ *)
 (* instantiate the simplifier                                               *)