diff -r 7edd3e5f26d4 -r 428385c4bc50 src/HOLCF/Ssum1.ML
--- a/src/HOLCF/Ssum1.ML	Tue Jul 04 14:58:40 2000 +0200
+++ b/src/HOLCF/Ssum1.ML	Tue Jul 04 15:58:11 2000 +0200
@@ -6,8 +6,6 @@
 Partial ordering for the strict sum ++
 *)
 
-local 
-
 fun eq_left s1 s2 = 
         (
         (res_inst_tac [("s",s1),("t",s2)] (inject_Isinl RS subst) 1)
@@ -36,174 +34,163 @@
         THEN (atac 2)
         THEN (etac sym 1))
 
-in
+val prems = goalw thy [less_ssum_def]
+"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)";
+by (cut_facts_tac prems 1);
+by (rtac select_equality 1);
+by (dtac conjunct1 2);
+by (dtac spec 2);
+by (dtac spec 2);
+by (etac mp 2);
+by (fast_tac HOL_cs 2);
+by (rtac conjI 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (eq_left "x" "u");
+by (eq_left "y" "xa");
+by (rtac refl 1);
+by (rtac conjI 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (UU_left "x");
+by (UU_right "v");
+by (Simp_tac 1);
+by (rtac conjI 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (eq_left "x" "u");
+by (UU_left "y");
+by (rtac iffI 1);
+by (etac UU_I 1);
+by (res_inst_tac [("s","x"),("t","UU::'a")] subst 1);
+by (atac 1);
+by (rtac refl_less 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (UU_left "x");
+by (UU_right "v");
+by (Simp_tac 1);
+qed "less_ssum1a";
+
 
-val less_ssum1a = prove_goalw thy [less_ssum_def]
-"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac select_equality 1),
-        (dtac conjunct1 2),
-        (dtac spec 2),
-        (dtac spec 2),
-        (etac mp 2),
-        (fast_tac HOL_cs 2),
-        (rtac conjI 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (eq_left "x" "u"),
-        (eq_left "y" "xa"),
-        (rtac refl 1),
-        (rtac conjI 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (UU_left "x"),
-        (UU_right "v"),
-        (Simp_tac 1),
-        (rtac conjI 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (eq_left "x" "u"),
-        (UU_left "y"),
-        (rtac iffI 1),
-        (etac UU_I 1),
-        (res_inst_tac [("s","x"),("t","UU::'a")] subst 1),
-        (atac 1),
-        (rtac refl_less 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (UU_left "x"),
-        (UU_right "v"),
-        (Simp_tac 1)
-        ]);
+val prems = goalw thy [less_ssum_def]
+"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)";
+by (cut_facts_tac prems 1);
+by (rtac select_equality 1);
+by (dtac conjunct2 2);
+by (dtac conjunct1 2);
+by (dtac spec 2);
+by (dtac spec 2);
+by (etac mp 2);
+by (fast_tac HOL_cs 2);
+by (rtac conjI 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (UU_right "x");
+by (UU_left "u");
+by (Simp_tac 1);
+by (rtac conjI 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (eq_right "x" "v");
+by (eq_right "y" "ya");
+by (rtac refl 1);
+by (rtac conjI 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (UU_right "x");
+by (UU_left "u");
+by (Simp_tac 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (eq_right "x" "v");
+by (UU_right "y");
+by (rtac iffI 1);
+by (etac UU_I 1);
+by (res_inst_tac [("s","UU::'b"),("t","x")] subst 1);
+by (etac sym 1);
+by (rtac refl_less 1);
+qed "less_ssum1b";
 
 
-val less_ssum1b = prove_goalw thy [less_ssum_def]
-"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac select_equality 1),
-        (dtac conjunct2 2),
-        (dtac conjunct1 2),
-        (dtac spec 2),
-        (dtac spec 2),
-        (etac mp 2),
-        (fast_tac HOL_cs 2),
-        (rtac conjI 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (UU_right "x"),
-        (UU_left "u"),
-        (Simp_tac 1),
-        (rtac conjI 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (eq_right "x" "v"),
-        (eq_right "y" "ya"),
-        (rtac refl 1),
-        (rtac conjI 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (UU_right "x"),
-        (UU_left "u"),
-        (Simp_tac 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (eq_right "x" "v"),
-        (UU_right "y"),
-        (rtac iffI 1),
-        (etac UU_I 1),
-        (res_inst_tac [("s","UU::'b"),("t","x")] subst 1),
-        (etac sym 1),
-        (rtac refl_less 1)
-        ]);
+val prems = goalw thy [less_ssum_def]
+"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)";
+by (cut_facts_tac prems 1);
+by (rtac select_equality 1);
+by (rtac conjI 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (eq_left  "x" "u");
+by (UU_left "xa");
+by (rtac iffI 1);
+by (res_inst_tac [("s","x"),("t","UU::'a")] subst 1);
+by (atac 1);
+by (rtac refl_less 1);
+by (etac UU_I 1);
+by (rtac conjI 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (UU_left "x");
+by (UU_right "v");
+by (Simp_tac 1);
+by (rtac conjI 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (eq_left  "x" "u");
+by (rtac refl 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (UU_left "x");
+by (UU_right "v");
+by (Simp_tac 1);
+by (dtac conjunct2 1);
+by (dtac conjunct2 1);
+by (dtac conjunct1 1);
+by (dtac spec 1);
+by (dtac spec 1);
+by (etac mp 1);
+by (fast_tac HOL_cs 1);
+qed "less_ssum1c";
 
 
-val less_ssum1c = prove_goalw thy [less_ssum_def]
-"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac select_equality 1),
-        (rtac conjI 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (eq_left  "x" "u"),
-        (UU_left "xa"),
-        (rtac iffI 1),
-        (res_inst_tac [("s","x"),("t","UU::'a")] subst 1),
-        (atac 1),
-        (rtac refl_less 1),
-        (etac UU_I 1),
-        (rtac conjI 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (UU_left "x"),
-        (UU_right "v"),
-        (Simp_tac 1),
-        (rtac conjI 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (eq_left  "x" "u"),
-        (rtac refl 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (UU_left "x"),
-        (UU_right "v"),
-        (Simp_tac 1),
-        (dtac conjunct2 1),
-        (dtac conjunct2 1),
-        (dtac conjunct1 1),
-        (dtac spec 1),
-        (dtac spec 1),
-        (etac mp 1),
-        (fast_tac HOL_cs 1)
-        ]);
-
-
-val less_ssum1d = prove_goalw thy [less_ssum_def]
-"[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac select_equality 1),
-        (dtac conjunct2 2),
-        (dtac conjunct2 2),
-        (dtac conjunct2 2),
-        (dtac spec 2),
-        (dtac spec 2),
-        (etac mp 2),
-        (fast_tac HOL_cs 2),
-        (rtac conjI 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (UU_right "x"),
-        (UU_left "u"),
-        (Simp_tac 1),
-        (rtac conjI 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (UU_right "ya"),
-        (eq_right "x" "v"),
-        (rtac iffI 1),
-        (etac UU_I 2),
-        (res_inst_tac [("s","UU"),("t","x")] subst 1),
-        (etac sym 1),
-        (rtac refl_less 1),
-        (rtac conjI 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (UU_right "x"),
-        (UU_left "u"),
-        (Simp_tac 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (eq_right "x" "v"),
-        (rtac refl 1)
-        ])
-end;
+val prems = goalw thy [less_ssum_def]
+"[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)";
+by (cut_facts_tac prems 1);
+by (rtac select_equality 1);
+by (dtac conjunct2 2);
+by (dtac conjunct2 2);
+by (dtac conjunct2 2);
+by (dtac spec 2);
+by (dtac spec 2);
+by (etac mp 2);
+by (fast_tac HOL_cs 2);
+by (rtac conjI 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (UU_right "x");
+by (UU_left "u");
+by (Simp_tac 1);
+by (rtac conjI 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (UU_right "ya");
+by (eq_right "x" "v");
+by (rtac iffI 1);
+by (etac UU_I 2);
+by (res_inst_tac [("s","UU"),("t","x")] subst 1);
+by (etac sym 1);
+by (rtac refl_less 1);
+by (rtac conjI 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (UU_right "x");
+by (UU_left "u");
+by (Simp_tac 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (eq_right "x" "v");
+by (rtac refl 1);
+qed "less_ssum1d";
 
 
 (* ------------------------------------------------------------------------ *)