# HG changeset patch
# User paulson
# Date 903024866 -7200
# Node ID 7a8975451a896cf14af9cb51651e2b893c172626
# Parent  c9ad6bbf3a34f92c30038672f52fad0258888d39
even more tidying of Goal commands

diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Arith.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -221,7 +221,7 @@
 qed "add_less_mono";
 
 (*A [clumsy] way of lifting < monotonicity to <= monotonicity *)
-val [lt_mono,le] = goal thy
+val [lt_mono,le] = Goal
      "[| !!i j::nat. i<j ==> f(i) < f(j);       \
 \        i <= j                                 \
 \     |] ==> f(i) <= (f(j)::nat)";
@@ -331,8 +331,8 @@
 
 (*** More results about difference ***)
 
-val [prem] = goal thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
-by (rtac (prem RS rev_mp) 1);
+Goal "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
+by (etac rev_mp 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "Suc_diff_n";
@@ -411,20 +411,20 @@
 by (ALLGOALS Asm_simp_tac);
 qed "le_imp_diff_is_add";
 
-val [prem] = goal thy "m < Suc(n) ==> m-n = 0";
-by (rtac (prem RS rev_mp) 1);
+Goal "m < Suc(n) ==> m-n = 0";
+by (etac rev_mp 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
 by (ALLGOALS Asm_simp_tac);
 qed "less_imp_diff_is_0";
 
-val prems = goal thy "m-n = 0  -->  n-m = 0  -->  m=n";
+Goal "m-n = 0  -->  n-m = 0  -->  m=n";
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (REPEAT(Simp_tac 1 THEN TRY(atac 1)));
 qed_spec_mp "diffs0_imp_equal";
 
-val [prem] = goal thy "m<n ==> 0<n-m";
-by (rtac (prem RS rev_mp) 1);
+Goal "m<n ==> 0<n-m";
+by (etac rev_mp 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "less_imp_diff_positive";
@@ -448,7 +448,7 @@
 by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));
 qed "zero_induct_lemma";
 
-val prems = goal thy "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
+val prems = Goal "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
 by (rtac (diff_self_eq_0 RS subst) 1);
 by (rtac (zero_induct_lemma RS mp RS mp) 1);
 by (REPEAT (ares_tac ([impI,allI]@prems) 1));
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Divides.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -10,7 +10,7 @@
 (** Less-then properties **)
 
 (*In ordinary notation: if 0<n and n<=m then m-n < m *)
-goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m";
+Goal "[| 0<n; ~ m<n |] ==> m - n < m";
 by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
 by (Blast_tac 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
@@ -200,9 +200,10 @@
  by (trans_tac 2);
 by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
 by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
- by (best_tac (claset() addIs [le_trans] 
-                       addss (simpset() addsimps [diff_less])) 1);
-by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 1));
+by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 2));
+br le_trans 1;
+by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [diff_less]) 1);
 qed "div_le_mono2";
 
 Goal "0<n ==> m div n <= m";
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Finite.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -11,7 +11,7 @@
 section "finite";
 
 (*Discharging ~ x:y entails extra work*)
-val major::prems = goal Finite.thy 
+val major::prems = Goal 
     "[| finite F;  P({}); \
 \       !!F x. [| finite F;  x ~: F;  P(F) |] ==> P(insert x F) \
 \    |] ==> P(F)";
@@ -21,7 +21,7 @@
 by (REPEAT (ares_tac prems 1));
 qed "finite_induct";
 
-val major::subs::prems = goal Finite.thy 
+val major::subs::prems = Goal 
     "[| finite F;  F <= A; \
 \       P({}); \
 \       !!F a. [| finite F; a:A; a ~: F;  P(F) |] ==> P(insert a F) \
@@ -35,10 +35,9 @@
 AddSIs Finites.intrs;
 
 (*The union of two finite sets is finite*)
-val major::prems = goal Finite.thy
-    "[| finite F;  finite G |] ==> finite(F Un G)";
-by (rtac (major RS finite_induct) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
+Goal "[| finite F;  finite G |] ==> finite(F Un G)";
+by (etac finite_induct 1);
+by (ALLGOALS Asm_simp_tac);
 qed "finite_UnI";
 
 (*Every subset of a finite set is finite*)
@@ -76,7 +75,7 @@
 by (Asm_simp_tac 1);
 qed "finite_imageI";
 
-val major::prems = goal Finite.thy 
+val major::prems = Goal 
     "[| finite c;  finite b;                                  \
 \       P(b);                                                   \
 \       !!x y. [| finite y;  x:y;  P(y) |] ==> P(y-{x}) \
@@ -87,7 +86,7 @@
                 (simpset() addsimps (prems@[Diff_subset RS finite_subset]))));
 val lemma = result();
 
-val prems = goal Finite.thy 
+val prems = Goal 
     "[| finite A;                                       \
 \       P(A);                                           \
 \       !!a A. [| finite A;  a:A;  P(A) |] ==> P(A-{a}) \
@@ -134,9 +133,8 @@
 
 (** The finite UNION of finite sets **)
 
-val [prem] = goal Finite.thy
- "finite A ==> (!a:A. finite(B a)) --> finite(UN a:A. B a)";
-by (rtac (prem RS finite_induct) 1);
+Goal "finite A ==> (!a:A. finite(B a)) --> finite(UN a:A. B a)";
+by (etac finite_induct 1);
 by (ALLGOALS Asm_simp_tac);
 bind_thm("finite_UnionI", ballI RSN (2, result() RS mp));
 Addsimps [finite_UnionI];
@@ -187,7 +185,7 @@
 
 section "Finite cardinality -- 'card'";
 
-goal Set.thy "{f i |i. (P i | i=n)} = insert (f n) {f i|i. P i}";
+Goal "{f i |i. (P i | i=n)} = insert (f n) {f i|i. P i}";
 by (Blast_tac 1);
 val Collect_conv_insert = result();
 
@@ -197,9 +195,8 @@
 qed "card_empty";
 Addsimps [card_empty];
 
-val [major] = goal Finite.thy
-  "finite A ==> ? (n::nat) f. A = {f i |i. i<n}";
-by (rtac (major RS finite_induct) 1);
+Goal "finite A ==> ? (n::nat) f. A = {f i |i. i<n}";
+by (etac finite_induct 1);
  by (res_inst_tac [("x","0")] exI 1);
  by (Simp_tac 1);
 by (etac exE 1);
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Fun.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -13,7 +13,7 @@
 by (rtac ext 1 THEN Asm_simp_tac 1);
 qed "expand_fun_eq";
 
-val prems = goal thy
+val prems = Goal
     "[| f(x)=u;  !!x. P(x) ==> g(f(x)) = x;  P(x) |] ==> x=g(u)";
 by (rtac (arg_cong RS box_equals) 1);
 by (REPEAT (resolve_tac (prems@[refl]) 1));
@@ -22,11 +22,11 @@
 
 (** "Axiom" of Choice, proved using the description operator **)
 
-goal HOL.thy "!!Q. ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
+Goal "!!Q. ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
 by (fast_tac (claset() addEs [selectI]) 1);
 qed "choice";
 
-goal Set.thy "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
+Goal "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
 by (fast_tac (claset() addEs [selectI]) 1);
 qed "bchoice";
 
@@ -57,44 +57,43 @@
 
 (*** inj(f): f is a one-to-one function ***)
 
-val prems = goalw thy [inj_def]
+val prems = Goalw [inj_def]
     "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
 by (blast_tac (claset() addIs prems) 1);
 qed "injI";
 
-val [major] = goal thy "(!!x. g(f(x)) = x) ==> inj(f)";
+val [major] = Goal "(!!x. g(f(x)) = x) ==> inj(f)";
 by (rtac injI 1);
 by (etac (arg_cong RS box_equals) 1);
 by (rtac major 1);
 by (rtac major 1);
 qed "inj_inverseI";
 
-val [major,minor] = goalw thy [inj_def]
-    "[| inj(f); f(x) = f(y) |] ==> x=y";
-by (rtac (major RS spec RS spec RS mp) 1);
-by (rtac minor 1);
+Goalw [inj_def] "[| inj(f); f(x) = f(y) |] ==> x=y";
+by (Blast_tac 1);
 qed "injD";
 
 (*Useful with the simplifier*)
-val [major] = goal thy "inj(f) ==> (f(x) = f(y)) = (x=y)";
+Goal "inj(f) ==> (f(x) = f(y)) = (x=y)";
 by (rtac iffI 1);
-by (etac (major RS injD) 1);
-by (etac arg_cong 1);
+by (etac arg_cong 2);
+by (etac injD 1);
+ba 1;
 qed "inj_eq";
 
-val [major] = goal thy "inj(f) ==> (@x. f(x)=f(y)) = y";
-by (rtac (major RS injD) 1);
+Goal "inj(f) ==> (@x. f(x)=f(y)) = y";
+by (etac injD 1);
 by (rtac selectI 1);
 by (rtac refl 1);
 qed "inj_select";
 
 (*A one-to-one function has an inverse (given using select).*)
-val [major] = goalw thy [inv_def] "inj(f) ==> inv f (f x) = x";
-by (EVERY1 [rtac (major RS inj_select)]);
+Goalw [inv_def] "inj(f) ==> inv f (f x) = x";
+by (etac inj_select 1);
 qed "inv_f_f";
 
 (* Useful??? *)
-val [oneone,minor] = goal thy
+val [oneone,minor] = Goal
     "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
 by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
 by (rtac (rangeI RS minor) 1);
@@ -103,60 +102,52 @@
 
 (*** inj_on f A: f is one-to-one over A ***)
 
-val prems = goalw thy [inj_on_def]
+val prems = Goalw [inj_on_def]
     "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_on f A";
 by (blast_tac (claset() addIs prems) 1);
 qed "inj_onI";
 
-val [major] = goal thy 
+val [major] = Goal 
     "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
 by (rtac inj_onI 1);
 by (etac (apply_inverse RS trans) 1);
 by (REPEAT (eresolve_tac [asm_rl,major] 1));
 qed "inj_on_inverseI";
 
-val major::prems = goalw thy [inj_on_def]
-    "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
-by (rtac (major RS bspec RS bspec RS mp) 1);
-by (REPEAT (resolve_tac prems 1));
+Goalw [inj_on_def] "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
+by (Blast_tac 1);
 qed "inj_onD";
 
 Goal "[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
 by (blast_tac (claset() addSDs [inj_onD]) 1);
 qed "inj_on_iff";
 
-val major::prems = goal thy
-    "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
-by (rtac contrapos 1);
-by (etac (major RS inj_onD) 2);
-by (REPEAT (resolve_tac prems 1));
+Goalw [inj_on_def] "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
+by (Blast_tac 1);
 qed "inj_on_contraD";
 
-Goalw [inj_on_def]
-    "[| A<=B; inj_on f B |] ==> inj_on f A";
+Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A";
 by (Blast_tac 1);
 qed "subset_inj_on";
 
 
 (*** Lemmas about inj ***)
 
-Goalw [o_def]
-    "[| inj(f);  inj_on g (range f) |] ==> inj(g o f)";
+Goalw [o_def] "[| inj(f);  inj_on g (range f) |] ==> inj(g o f)";
 by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1);
 qed "comp_inj";
 
-val [prem] = goal thy "inj(f) ==> inj_on f A";
-by (blast_tac (claset() addIs [prem RS injD, inj_onI]) 1);
+Goal "inj(f) ==> inj_on f A";
+by (blast_tac (claset() addIs [injD, inj_onI]) 1);
 qed "inj_imp";
 
-val [prem] = goalw thy [inv_def] "y : range(f) ==> f(inv f y) = y";
-by (EVERY1 [rtac (prem RS rangeE), rtac selectI, etac sym]);
+Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
+by (fast_tac (claset() addIs [selectI]) 1);
 qed "f_inv_f";
 
-val prems = goal thy
-    "[| inv f x=inv f y; x: range(f);  y: range(f) |] ==> x=y";
+Goal "[| inv f x=inv f y; x: range(f);  y: range(f) |] ==> x=y";
 by (rtac (arg_cong RS box_equals) 1);
-by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1));
+by (REPEAT (ares_tac [f_inv_f] 1));
 qed "inv_injective";
 
 Goal "[| inj(f);  A<=range(f) |] ==> inj_on (inv f) A";
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/Gfp.ML
--- a/src/HOL/Gfp.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Gfp.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -22,18 +22,18 @@
 by (etac CollectD 1);
 qed "gfp_least";
 
-val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) <= f(gfp(f))";
+Goal "mono(f) ==> gfp(f) <= f(gfp(f))";
 by (EVERY1 [rtac gfp_least, rtac subset_trans, atac,
-            rtac (mono RS monoD), rtac gfp_upperbound, atac]);
+            etac monoD, rtac gfp_upperbound, atac]);
 qed "gfp_lemma2";
 
-val [mono] = goal Gfp.thy "mono(f) ==> f(gfp(f)) <= gfp(f)";
-by (EVERY1 [rtac gfp_upperbound, rtac (mono RS monoD), 
-            rtac gfp_lemma2, rtac mono]);
+Goal "mono(f) ==> f(gfp(f)) <= gfp(f)";
+by (EVERY1 [rtac gfp_upperbound, rtac monoD, assume_tac,
+            etac gfp_lemma2]);
 qed "gfp_lemma3";
 
-val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) = f(gfp(f))";
-by (REPEAT (resolve_tac [equalityI,gfp_lemma2,gfp_lemma3,mono] 1));
+Goal "mono(f) ==> gfp(f) = f(gfp(f))";
+by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1));
 qed "gfp_Tarski";
 
 (*** Coinduction rules for greatest fixed points ***)
@@ -70,8 +70,8 @@
          - instead of the condition  X <= f(X)
                            consider  X <= (f(X) Un f(f(X)) ...) Un gfp(X) ***)
 
-val [prem] = goal Gfp.thy "mono(f) ==> mono(%x. f(x) Un X Un B)";
-by (REPEAT (ares_tac [subset_refl, monoI, Un_mono, prem RS monoD] 1));
+Goal "mono(f) ==> mono(%x. f(x) Un X Un B)";
+by (REPEAT (ares_tac [subset_refl, monoI, Un_mono] 1 ORELSE etac monoD 1));
 qed "coinduct3_mono_lemma";
 
 val [prem,mono] = goal Gfp.thy
@@ -88,12 +88,11 @@
 by (rtac Un_upper2 1);
 qed "coinduct3_lemma";
 
-val prems = goal Gfp.thy
-    "[| mono(f);  a:X;  X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)";
+Goal
+  "[| mono(f);  a:X;  X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)";
 by (rtac (coinduct3_lemma RSN (2,weak_coinduct)) 1);
-by (resolve_tac (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1);
-by (rtac (UnI2 RS UnI1) 1);
-by (REPEAT (resolve_tac prems 1));
+by (resolve_tac [coinduct3_mono_lemma RS lfp_Tarski RS ssubst] 1);
+by Auto_tac;
 qed "coinduct3";
 
 
@@ -111,7 +110,7 @@
 qed "def_coinduct";
 
 (*The version used in the induction/coinduction package*)
-val prems = goal Gfp.thy
+val prems = Goal
     "[| A == gfp(%w. Collect(P(w)));  mono(%w. Collect(P(w)));  \
 \       a: X;  !!z. z: X ==> P (X Un A) z |] ==> \
 \    a : A";
@@ -126,7 +125,7 @@
 qed "def_coinduct3";
 
 (*Monotonicity of gfp!*)
-val [prem] = goal Gfp.thy "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)";
+val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)";
 by (rtac (gfp_upperbound RS gfp_least) 1);
 by (etac (prem RSN (2,subset_trans)) 1);
 qed "gfp_mono";
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/Integ/Integ.ML
--- a/src/HOL/Integ/Integ.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Integ/Integ.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -32,10 +32,8 @@
 
 (** Natural deduction for intrel **)
 
-val prems = goalw Integ.thy [intrel_def]
-    "[| x1+y2 = x2+y1|] ==> \
-\    ((x1,y1),(x2,y2)): intrel";
-by (fast_tac (claset() addIs prems) 1);
+Goalw  [intrel_def] "[| x1+y2 = x2+y1|] ==> ((x1,y1),(x2,y2)): intrel";
+by (Fast_tac 1);
 qed "intrelI";
 
 (*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
@@ -45,7 +43,7 @@
 by (Fast_tac 1);
 qed "intrelE_lemma";
 
-val [major,minor] = goal Integ.thy
+val [major,minor] = Goal
   "[| p: intrel;  \
 \     !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2));  x1+y2 = x2+y1|] ==> Q |] \
 \  ==> Q";
@@ -130,8 +128,7 @@
 qed "zminus";
 
 (*by lcp*)
-val [prem] = goal Integ.thy
-    "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P";
+val [prem] = Goal "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P";
 by (res_inst_tac [("x1","z")] 
     (rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1);
 by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1);
@@ -159,8 +156,7 @@
 (**** znegative: the test for negative integers ****)
 
 
-Goalw [znegative_def, znat_def]
-    "~ znegative($# n)";
+Goalw [znegative_def, znat_def] "~ znegative($# n)";
 by (Simp_tac 1);
 by Safe_tac;
 qed "not_znegative_znat";
@@ -445,13 +441,11 @@
 by (Simp_tac 1);
 qed "zminus_zpred";
 
-Goalw [zsuc_def,zpred_def,zdiff_def]
-   "zpred(zsuc(z)) = z";
+Goalw [zsuc_def,zpred_def,zdiff_def]  "zpred(zsuc(z)) = z";
 by (simp_tac (simpset() addsimps [zadd_assoc]) 1);
 qed "zpred_zsuc";
 
-Goalw [zsuc_def,zpred_def,zdiff_def]
-   "zsuc(zpred(z)) = z";
+Goalw [zsuc_def,zpred_def,zdiff_def]  "zsuc(zpred(z)) = z";
 by (simp_tac (simpset() addsimps [zadd_assoc]) 1);
 qed "zsuc_zpred";
 
@@ -473,13 +467,13 @@
 by (rtac zminus_zminus 1);
 qed "zminus_exchange";
 
-Goal"(zsuc(z)=zsuc(w)) = (z=w)";
+Goal "(zsuc(z)=zsuc(w)) = (z=w)";
 by Safe_tac;
 by (dres_inst_tac [("f","zpred")] arg_cong 1);
 by (asm_full_simp_tac (simpset() addsimps [zpred_zsuc]) 1);
 qed "bijective_zsuc";
 
-Goal"(zpred(z)=zpred(w)) = (z=w)";
+Goal "(zpred(z)=zpred(w)) = (z=w)";
 by Safe_tac;
 by (dres_inst_tac [("f","zsuc")] arg_cong 1);
 by (asm_full_simp_tac (simpset() addsimps [zsuc_zpred]) 1);
@@ -579,7 +573,7 @@
 
 val zless_zsucI = zlessI RSN (2,zless_trans);
 
-Goal "!!z w::int. z<w ==> ~w<z";
+Goal "!!w::int. z<w ==> ~w<z";
 by (safe_tac (claset() addSDs [zless_eq_zadd_Suc]));
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by Safe_tac;
@@ -611,7 +605,7 @@
 by (asm_full_simp_tac
     (simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
 by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
-by (REPEAT (fast_tac (claset() addss (simpset() addsimps add_ac)) 1));
+by (auto_tac (claset(), simpset() addsimps add_ac));
 qed "zless_linear";
 
 
@@ -664,14 +658,15 @@
 by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq]) 1);
 qed "zle_refl";
 
-val prems = goal Integ.thy "!!i. [| i <= j; j < k |] ==> i < (k::int)";
+Goal "[| i <= j; j < k |] ==> i < (k::int)";
 by (dtac zle_imp_zless_or_eq 1);
 by (fast_tac (claset() addIs [zless_trans]) 1);
 qed "zle_zless_trans";
 
 Goal "[| i <= j; j <= k |] ==> i <= (k::int)";
 by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
-            rtac zless_or_eq_imp_zle, fast_tac (claset() addIs [zless_trans])]);
+            rtac zless_or_eq_imp_zle, 
+	    fast_tac (claset() addIs [zless_trans])]);
 qed "zle_trans";
 
 Goal "[| z <= w; w <= z |] ==> z = (w::int)";
@@ -680,7 +675,7 @@
 qed "zle_anti_sym";
 
 
-Goal "!!w w' z::int. z + w' = z + w ==> w' = w";
+Goal "!!w::int. z + w' = z + w ==> w' = w";
 by (dres_inst_tac [("f", "%x. x + $~z")] arg_cong 1);
 by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
 qed "zadd_left_cancel";
@@ -688,19 +683,19 @@
 
 (*** Monotonicity results ***)
 
-Goal "!!v w z::int. v < w ==> v + z < w + z";
+Goal "!!z::int. v < w ==> v + z < w + z";
 by (safe_tac (claset() addSDs [zless_eq_zadd_Suc]));
 by (simp_tac (simpset() addsimps zadd_ac) 1);
 by (simp_tac (simpset() addsimps [zadd_assoc RS sym, zless_zadd_Suc]) 1);
 qed "zadd_zless_mono1";
 
-Goal "!!v w z::int. (v+z < w+z) = (v < w)";
+Goal "!!z::int. (v+z < w+z) = (v < w)";
 by (safe_tac (claset() addSEs [zadd_zless_mono1]));
 by (dres_inst_tac [("z", "$~z")] zadd_zless_mono1 1);
 by (asm_full_simp_tac (simpset() addsimps [zadd_assoc]) 1);
 qed "zadd_left_cancel_zless";
 
-Goal "!!v w z::int. (v+z <= w+z) = (v <= w)";
+Goal "!!z::int. (v+z <= w+z) = (v <= w)";
 by (asm_full_simp_tac
     (simpset() addsimps [zle_def, zadd_left_cancel_zless]) 1);
 qed "zadd_left_cancel_zle";
@@ -709,14 +704,14 @@
 bind_thm ("zadd_zle_mono1", zadd_left_cancel_zle RS iffD2);
 
 
-Goal "!!z' z::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z";
+Goal "!!z z'::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z";
 by (etac (zadd_zle_mono1 RS zle_trans) 1);
 by (simp_tac (simpset() addsimps [zadd_commute]) 1);
 (*w moves to the end because it is free while z', z are bound*)
 by (etac zadd_zle_mono1 1);
 qed "zadd_zle_mono";
 
-Goal "!!w z::int. z<=$#0 ==> w+z <= w";
+Goal "!!z::int. z<=$#0 ==> w+z <= w";
 by (dres_inst_tac [("z", "w")] zadd_zle_mono1 1);
 by (asm_full_simp_tac (simpset() addsimps [zadd_commute]) 1);
 qed "zadd_zle_self";
@@ -726,7 +721,7 @@
 
 (** One auxiliary theorem...**)
 
-goal HOL.thy "(x = False) = (~ x)";
+Goal "(x = False) = (~ x)";
   by (fast_tac HOL_cs 1);
 qed "eq_False_conv";
 
@@ -848,8 +843,7 @@
 
 (* a case theorem distinguishing positive and negative int *)  
 
-val prems = goal Integ.thy 
-    "[|!! n. P ($# n); !! n. P ($~ $# Suc n) |] ==> P z"; 
+val prems = Goal "[|!! n. P ($# n); !! n. P ($~ $# Suc n) |] ==> P z"; 
   by (cut_inst_tac [("P","znegative z")] excluded_middle 1); 
   by (fast_tac (HOL_cs addSDs[znegativeD,not_znegativeD] addSIs prems) 1); 
 qed "int_cases"; 
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/Lfp.ML
--- a/src/HOL/Lfp.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Lfp.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-For lfp.thy.  The Knaster-Tarski Theorem
+The Knaster-Tarski Theorem
 *)
 
 open Lfp;
@@ -12,34 +12,34 @@
 
 (* lfp(f) is the greatest lower bound of {u. f(u) <= u} *)
 
-val prems = goalw Lfp.thy [lfp_def] "[| f(A) <= A |] ==> lfp(f) <= A";
+Goalw [lfp_def] "f(A) <= A ==> lfp(f) <= A";
 by (rtac (CollectI RS Inter_lower) 1);
-by (resolve_tac prems 1);
+by (assume_tac 1);
 qed "lfp_lowerbound";
 
-val prems = goalw Lfp.thy [lfp_def]
+val prems = Goalw [lfp_def]
     "[| !!u. f(u) <= u ==> A<=u |] ==> A <= lfp(f)";
 by (REPEAT (ares_tac ([Inter_greatest]@prems) 1));
 by (etac CollectD 1);
 qed "lfp_greatest";
 
-val [mono] = goal Lfp.thy "mono(f) ==> f(lfp(f)) <= lfp(f)";
+Goal "mono(f) ==> f(lfp(f)) <= lfp(f)";
 by (EVERY1 [rtac lfp_greatest, rtac subset_trans,
-            rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]);
+            etac monoD, rtac lfp_lowerbound, atac, atac]);
 qed "lfp_lemma2";
 
-val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) <= f(lfp(f))";
-by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD), 
-            rtac lfp_lemma2, rtac mono]);
+Goal "mono(f) ==> lfp(f) <= f(lfp(f))";
+by (EVERY1 [rtac lfp_lowerbound, rtac monoD, assume_tac,
+            etac lfp_lemma2]);
 qed "lfp_lemma3";
 
-val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) = f(lfp(f))";
-by (REPEAT (resolve_tac [equalityI,lfp_lemma2,lfp_lemma3,mono] 1));
+Goal "mono(f) ==> lfp(f) = f(lfp(f))";
+by (REPEAT (ares_tac [equalityI,lfp_lemma2,lfp_lemma3] 1));
 qed "lfp_Tarski";
 
 (*** General induction rule for least fixed points ***)
 
-val [lfp,mono,indhyp] = goal Lfp.thy
+val [lfp,mono,indhyp] = Goal
     "[| a: lfp(f);  mono(f);                            \
 \       !!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)   \
 \    |] ==> P(a)";
@@ -62,7 +62,7 @@
 by (rtac (mono RS lfp_Tarski) 1);
 qed "def_lfp_Tarski";
 
-val rew::prems = goal Lfp.thy
+val rew::prems = Goal
     "[| A == lfp(f);  mono(f);   a:A;                   \
 \       !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x)        \
 \    |] ==> P(a)";
@@ -71,7 +71,7 @@
 qed "def_induct";
 
 (*Monotonicity of lfp!*)
-val [prem] = goal Lfp.thy "[| !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)";
+val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)";
 by (rtac (lfp_lowerbound RS lfp_greatest) 1);
 by (etac (prem RS subset_trans) 1);
 qed "lfp_mono";
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/List.ML
--- a/src/HOL/List.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/List.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -8,14 +8,14 @@
 
 Goal "!x. xs ~= x#xs";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed_spec_mp "not_Cons_self";
 bind_thm("not_Cons_self2",not_Cons_self RS not_sym);
 Addsimps [not_Cons_self,not_Cons_self2];
 
 Goal "(xs ~= []) = (? y ys. xs = y#ys)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "neq_Nil_conv";
 
 (* Induction over the length of a list: *)
@@ -71,43 +71,43 @@
 
 Goal "length(xs@ys) = length(xs)+length(ys)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed"length_append";
 Addsimps [length_append];
 
 Goal "length (map f xs) = length xs";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "length_map";
 Addsimps [length_map];
 
 Goal "length(rev xs) = length(xs)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "length_rev";
 Addsimps [length_rev];
 
 Goal "xs ~= [] ==> length(tl xs) = (length xs) - 1";
 by (exhaust_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "length_tl";
 Addsimps [length_tl];
 
 Goal "(length xs = 0) = (xs = [])";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "length_0_conv";
 AddIffs [length_0_conv];
 
 Goal "(0 = length xs) = (xs = [])";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "zero_length_conv";
 AddIffs [zero_length_conv];
 
 Goal "(0 < length xs) = (xs ~= [])";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "length_greater_0_conv";
 AddIffs [length_greater_0_conv];
 
@@ -123,36 +123,36 @@
 
 Goal "(xs@ys)@zs = xs@(ys@zs)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "append_assoc";
 Addsimps [append_assoc];
 
 Goal "xs @ [] = xs";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "append_Nil2";
 Addsimps [append_Nil2];
 
 Goal "(xs@ys = []) = (xs=[] & ys=[])";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "append_is_Nil_conv";
 AddIffs [append_is_Nil_conv];
 
 Goal "([] = xs@ys) = (xs=[] & ys=[])";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "Nil_is_append_conv";
 AddIffs [Nil_is_append_conv];
 
 Goal "(xs @ ys = xs) = (ys=[])";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "append_self_conv";
 
 Goal "(xs = xs @ ys) = (ys=[])";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "self_append_conv";
 AddIffs [append_self_conv,self_append_conv];
 
@@ -192,7 +192,7 @@
 
 Goal "(xs @ ys = ys) = (xs=[])";
 by (cut_inst_tac [("zs","[]")] append_same_eq 1);
-by (Auto_tac);
+by Auto_tac;
 qed "append_self_conv2";
 
 Goal "(ys = xs @ ys) = (xs=[])";
@@ -204,13 +204,13 @@
 
 Goal "xs ~= [] --> hd xs # tl xs = xs";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed_spec_mp "hd_Cons_tl";
 Addsimps [hd_Cons_tl];
 
 Goal "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "hd_append";
 
 Goal "xs ~= [] ==> hd(xs @ ys) = hd xs";
@@ -252,31 +252,31 @@
 
 Goal "(!x. x : set xs --> f x = g x) --> map f xs = map g xs";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
 
 Goal "map (%x. x) = (%xs. xs)";
 by (rtac ext 1);
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "map_ident";
 Addsimps[map_ident];
 
 Goal "map f (xs@ys) = map f xs @ map f ys";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "map_append";
 Addsimps[map_append];
 
 Goalw [o_def] "map (f o g) xs = map f (map g xs)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "map_compose";
 Addsimps[map_compose];
 
 Goal "rev(map f xs) = map f (rev xs)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "rev_map";
 
 (* a congruence rule for map: *)
@@ -284,19 +284,19 @@
 by (rtac impI 1);
 by (hyp_subst_tac 1);
 by (induct_tac "ys" 1);
-by (Auto_tac);
+by Auto_tac;
 val lemma = result();
 bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp)));
 
 Goal "(map f xs = []) = (xs = [])";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "map_is_Nil_conv";
 AddIffs [map_is_Nil_conv];
 
 Goal "([] = map f xs) = (xs = [])";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "Nil_is_map_conv";
 AddIffs [Nil_is_map_conv];
 
@@ -307,25 +307,25 @@
 
 Goal "rev(xs@ys) = rev(ys) @ rev(xs)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "rev_append";
 Addsimps[rev_append];
 
 Goal "rev(rev l) = l";
 by (induct_tac "l" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "rev_rev_ident";
 Addsimps[rev_rev_ident];
 
 Goal "(rev xs = []) = (xs = [])";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "rev_is_Nil_conv";
 AddIffs [rev_is_Nil_conv];
 
 Goal "([] = rev xs) = (xs = [])";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "Nil_is_rev_conv";
 AddIffs [Nil_is_rev_conv];
 
@@ -341,7 +341,7 @@
 
 Goal  "(xs = [] --> P) -->  (!ys y. xs = ys@[y] --> P) --> P";
 by (res_inst_tac [("xs","xs")] rev_induct 1);
-by (Auto_tac);
+by Auto_tac;
 bind_thm ("rev_exhaust",
   impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
 
@@ -352,13 +352,13 @@
 
 Goal "x mem (xs@ys) = (x mem xs | x mem ys)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "mem_append";
 Addsimps[mem_append];
 
 Goal "x mem [x:xs. P(x)] = (x mem xs & P(x))";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "mem_filter";
 Addsimps[mem_filter];
 
@@ -373,40 +373,40 @@
 
 Goal "set (xs@ys) = (set xs Un set ys)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "set_append";
 Addsimps[set_append];
 
 Goal "(x mem xs) = (x: set xs)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "set_mem_eq";
 
 Goal "set l <= set (x#l)";
-by (Auto_tac);
+by Auto_tac;
 qed "set_subset_Cons";
 
 Goal "(set xs = {}) = (xs = [])";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "set_empty";
 Addsimps [set_empty];
 
 Goal "set(rev xs) = set(xs)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "set_rev";
 Addsimps [set_rev];
 
 Goal "set(map f xs) = f``(set xs)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "set_map";
 Addsimps [set_map];
 
 Goal "(x : set(filter P xs)) = (x : set xs & P x)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "in_set_filter";
 Addsimps [in_set_filter];
 
@@ -418,14 +418,14 @@
 by(blast_tac (claset() addIs [eq_Nil_appendI,Cons_eq_appendI]) 1);
 by(REPEAT(etac exE 1));
 by(exhaust_tac "ys" 1);
-by(Auto_tac);
+by Auto_tac;
 qed "in_set_conv_decomp";
 
 (* eliminate `lists' in favour of `set' *)
 
 Goal "(xs : lists A) = (!x : set xs. x : A)";
 by(induct_tac "xs" 1);
-by(Auto_tac);
+by Auto_tac;
 qed "in_lists_conv_set";
 
 bind_thm("in_listsD",in_lists_conv_set RS iffD1);
@@ -439,19 +439,19 @@
 
 Goal "list_all (%x. True) xs = True";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "list_all_True";
 Addsimps [list_all_True];
 
 Goal "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "list_all_append";
 Addsimps [list_all_append];
 
 Goal "list_all P xs = (!x. x mem xs --> P(x))";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "list_all_mem_conv";
 
 
@@ -461,25 +461,25 @@
 
 Goal "filter P (xs@ys) = filter P xs @ filter P ys";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "filter_append";
 Addsimps [filter_append];
 
 Goal "filter (%x. True) xs = xs";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "filter_True";
 Addsimps [filter_True];
 
 Goal "filter (%x. False) xs = []";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "filter_False";
 Addsimps [filter_False];
 
 Goal "length (filter P xs) <= length xs";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "length_filter";
 
 
@@ -489,41 +489,41 @@
 
 Goal  "concat(xs@ys) = concat(xs)@concat(ys)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed"concat_append";
 Addsimps [concat_append];
 
 Goal "(concat xss = []) = (!xs:set xss. xs=[])";
 by (induct_tac "xss" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "concat_eq_Nil_conv";
 AddIffs [concat_eq_Nil_conv];
 
 Goal "([] = concat xss) = (!xs:set xss. xs=[])";
 by (induct_tac "xss" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "Nil_eq_concat_conv";
 AddIffs [Nil_eq_concat_conv];
 
 Goal  "set(concat xs) = Union(set `` set xs)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed"set_concat";
 Addsimps [set_concat];
 
 Goal "map f (concat xs) = concat (map (map f) xs)"; 
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "map_concat";
 
 Goal "filter p (concat xs) = concat (map (filter p) xs)"; 
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed"filter_concat"; 
 
 Goal "rev(concat xs) = concat (map rev (rev xs))";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "rev_concat";
 
 (** nth **)
@@ -535,7 +535,7 @@
  by (Asm_simp_tac 1);
  by (rtac allI 1);
  by (exhaust_tac "xs" 1);
-  by (Auto_tac);
+  by Auto_tac;
 qed_spec_mp "nth_append";
 
 Goal "!n. n < length xs --> (map f xs)!n = f(xs!n)";
@@ -545,7 +545,7 @@
 (* case x#xl *)
 by (rtac allI 1);
 by (induct_tac "n" 1);
-by (Auto_tac);
+by Auto_tac;
 qed_spec_mp "nth_map";
 Addsimps [nth_map];
 
@@ -556,7 +556,7 @@
 (* case x#xl *)
 by (rtac allI 1);
 by (induct_tac "n" 1);
-by (Auto_tac);
+by Auto_tac;
 qed_spec_mp "list_all_nth";
 
 Goal "!n. n < length xs --> xs!n mem xs";
@@ -589,30 +589,30 @@
 
 Goal "last(xs@[x]) = x";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "last_snoc";
 Addsimps [last_snoc];
 
 Goal "butlast(xs@[x]) = xs";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "butlast_snoc";
 Addsimps [butlast_snoc];
 
 Goal "length(butlast xs) = length xs - 1";
 by (res_inst_tac [("xs","xs")] rev_induct 1);
-by (Auto_tac);
+by Auto_tac;
 qed "length_butlast";
 Addsimps [length_butlast];
 
 Goal "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed_spec_mp "butlast_append";
 
 Goal "x:set(butlast xs) --> x:set xs";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed_spec_mp "in_set_butlastD";
 
 Goal "x:set(butlast xs) ==> x:set(butlast(xs@ys))";
@@ -631,12 +631,12 @@
 
 Goal "take 0 xs = []";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "take_0";
 
 Goal "drop 0 xs = xs";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "drop_0";
 
 Goal "take (Suc n) (x#xs) = x # take n xs";
@@ -652,102 +652,102 @@
 
 Goal "!xs. length(take n xs) = min (length xs) n";
 by (induct_tac "n" 1);
- by (Auto_tac);
+ by Auto_tac;
 by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
 qed_spec_mp "length_take";
 Addsimps [length_take];
 
 Goal "!xs. length(drop n xs) = (length xs - n)";
 by (induct_tac "n" 1);
- by (Auto_tac);
+ by Auto_tac;
 by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
 qed_spec_mp "length_drop";
 Addsimps [length_drop];
 
 Goal "!xs. length xs <= n --> take n xs = xs";
 by (induct_tac "n" 1);
- by (Auto_tac);
+ by Auto_tac;
 by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
 qed_spec_mp "take_all";
 
 Goal "!xs. length xs <= n --> drop n xs = []";
 by (induct_tac "n" 1);
- by (Auto_tac);
+ by Auto_tac;
 by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
 qed_spec_mp "drop_all";
 
 Goal "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
 by (induct_tac "n" 1);
- by (Auto_tac);
+ by Auto_tac;
 by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
 qed_spec_mp "take_append";
 Addsimps [take_append];
 
 Goal "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 
 by (induct_tac "n" 1);
- by (Auto_tac);
+ by Auto_tac;
 by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
 qed_spec_mp "drop_append";
 Addsimps [drop_append];
 
 Goal "!xs n. take n (take m xs) = take (min n m) xs"; 
 by (induct_tac "m" 1);
- by (Auto_tac);
+ by Auto_tac;
 by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
 by (exhaust_tac "na" 1);
- by (Auto_tac);
+ by Auto_tac;
 qed_spec_mp "take_take";
 
 Goal "!xs. drop n (drop m xs) = drop (n + m) xs"; 
 by (induct_tac "m" 1);
- by (Auto_tac);
+ by Auto_tac;
 by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
 qed_spec_mp "drop_drop";
 
 Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
 by (induct_tac "m" 1);
- by (Auto_tac);
+ by Auto_tac;
 by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
 qed_spec_mp "take_drop";
 
 Goal "!xs. take n (map f xs) = map f (take n xs)"; 
 by (induct_tac "n" 1);
- by (Auto_tac);
+ by Auto_tac;
 by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
 qed_spec_mp "take_map"; 
 
 Goal "!xs. drop n (map f xs) = map f (drop n xs)"; 
 by (induct_tac "n" 1);
- by (Auto_tac);
+ by Auto_tac;
 by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
 qed_spec_mp "drop_map";
 
 Goal "!n i. i < n --> (take n xs)!i = xs!i";
 by (induct_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
 by (exhaust_tac "n" 1);
  by (Blast_tac 1);
 by (exhaust_tac "i" 1);
- by (Auto_tac);
+ by Auto_tac;
 qed_spec_mp "nth_take";
 Addsimps [nth_take];
 
 Goal  "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";
 by (induct_tac "n" 1);
- by (Auto_tac);
+ by Auto_tac;
 by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
 qed_spec_mp "nth_drop";
 Addsimps [nth_drop];
 
@@ -757,37 +757,37 @@
 
 Goal "takeWhile P xs @ dropWhile P xs = xs";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "takeWhile_dropWhile_id";
 Addsimps [takeWhile_dropWhile_id];
 
 Goal  "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 bind_thm("takeWhile_append1", conjI RS (result() RS mp));
 Addsimps [takeWhile_append1];
 
 Goal "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 bind_thm("takeWhile_append2", ballI RS (result() RS mp));
 Addsimps [takeWhile_append2];
 
 Goal "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 bind_thm("dropWhile_append1", conjI RS (result() RS mp));
 Addsimps [dropWhile_append1];
 
 Goal "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 bind_thm("dropWhile_append2", ballI RS (result() RS mp));
 Addsimps [dropWhile_append2];
 
 Goal "x:set(takeWhile P xs) --> x:set xs & P x";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed_spec_mp"set_take_whileD";
 
 qed_goal "zip_Nil_Nil"   thy "zip []     []     = []" (K [Simp_tac 1]);
@@ -800,7 +800,7 @@
 
 Goal "!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys";
 by(induct_tac "xs" 1);
-by(Auto_tac);
+by Auto_tac;
 qed_spec_mp "foldl_append";
 Addsimps [foldl_append];
 
@@ -821,7 +821,7 @@
 
 Goal "!m. (foldl op+ m ns = 0) = (m=0 & (!n : set ns. n=0))";
 by(induct_tac "ns" 1);
-by(Auto_tac);
+by Auto_tac;
 qed_spec_mp "sum_eq_0_conv";
 AddIffs [sum_eq_0_conv];
 
@@ -838,12 +838,12 @@
 
 Goal "nodups(remdups xs)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "nodups_remdups";
 
 Goal "nodups xs --> nodups (filter P xs)";
 by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
 qed_spec_mp "nodups_filter";
 
 (** replicate **)
@@ -851,7 +851,7 @@
 
 Goal "set(replicate (Suc n) x) = {x}";
 by (induct_tac "n" 1);
-by (Auto_tac);
+by Auto_tac;
 val lemma = result();
 
 Goal "n ~= 0 ==> set(replicate n x) = {x}";
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Nat.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -9,12 +9,12 @@
 val [nat_rec_0, nat_rec_Suc] = nat.recs;
 
 (*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
-val prems = goal thy
+val prems = Goal
     "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c";
 by (simp_tac (simpset() addsimps prems) 1);
 qed "def_nat_rec_0";
 
-val prems = goal thy
+val prems = Goal
     "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)";
 by (simp_tac (simpset() addsimps prems) 1);
 qed "def_nat_rec_Suc";
@@ -26,9 +26,8 @@
 by (REPEAT (Blast_tac 1));
 qed "not0_implies_Suc";
 
-val prems = goal thy "m<n ==> n ~= 0";
+Goal "m<n ==> n ~= 0";
 by (exhaust_tac "n" 1);
-by (cut_facts_tac prems 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "gr_implies_not0";
 
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/NatDef.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -20,22 +20,22 @@
 by (rtac (singletonI RS UnI1) 1);
 qed "Zero_RepI";
 
-val prems = goal thy "i: Nat ==> Suc_Rep(i) : Nat";
+Goal "i: Nat ==> Suc_Rep(i) : Nat";
 by (stac Nat_unfold 1);
 by (rtac (imageI RS UnI2) 1);
-by (resolve_tac prems 1);
+by (assume_tac 1);
 qed "Suc_RepI";
 
 (*** Induction ***)
 
-val major::prems = goal thy
+val major::prems = Goal
     "[| i: Nat;  P(Zero_Rep);   \
 \       !!j. [| j: Nat; P(j) |] ==> P(Suc_Rep(j)) |]  ==> P(i)";
 by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_induct) 1);
 by (blast_tac (claset() addIs prems) 1);
 qed "Nat_induct";
 
-val prems = goalw thy [Zero_def,Suc_def]
+val prems = Goalw [Zero_def,Suc_def]
     "[| P(0);   \
 \       !!n. P(n) ==> P(Suc(n)) |]  ==> P(n)";
 by (rtac (Rep_Nat_inverse RS subst) 1);   (*types force good instantiation*)
@@ -49,7 +49,7 @@
   res_inst_tac [("n",a)] nat_induct i  THEN  rename_last_tac a [""] (i+1);
 
 (*A special form of induction for reasoning about m<n and m-n*)
-val prems = goal thy
+val prems = Goal
     "[| !!x. P x 0;  \
 \       !!y. P 0 (Suc y);  \
 \       !!x y. [| P x y |] ==> P (Suc x) (Suc y)  \
@@ -131,10 +131,10 @@
 
 (** Introduction properties **)
 
-val prems = goalw thy [less_def] "[| i<j;  j<k |] ==> i<(k::nat)";
+Goalw [less_def] "[| i<j;  j<k |] ==> i<(k::nat)";
 by (rtac (trans_trancl RS transD) 1);
-by (resolve_tac prems 1);
-by (resolve_tac prems 1);
+by (assume_tac 1);
+by (assume_tac 1);
 qed "less_trans";
 
 Goalw [less_def, pred_nat_def] "n < Suc(n)";
@@ -156,8 +156,8 @@
 
 (** Elimination properties **)
 
-val prems = goalw thy [less_def] "n<m ==> ~ m<(n::nat)";
-by (blast_tac (claset() addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
+Goalw [less_def] "n<m ==> ~ m<(n::nat)";
+by (blast_tac (claset() addIs [wf_pred_nat, wf_trancl RS wf_asym])1);
 qed "less_not_sym";
 
 (* [| n<m; m<n |] ==> R *)
@@ -176,7 +176,7 @@
 qed "less_not_refl2";
 
 
-val major::prems = goalw thy [less_def, pred_nat_def]
+val major::prems = Goalw [less_def, pred_nat_def]
     "[| i<k;  k=Suc(i) ==> P;  !!j. [| i<j;  k=Suc(j) |] ==> P \
 \    |] ==> P";
 by (rtac (major RS tranclE) 1);
@@ -197,7 +197,7 @@
 (* n<0 ==> R *)
 bind_thm ("less_zeroE", not_less0 RS notE);
 
-val [major,less,eq] = goal thy
+val [major,less,eq] = Goal
     "[| m < Suc(n);  m<n ==> P;  m=n ==> P |] ==> P";
 by (rtac (major RS lessE) 1);
 by (rtac eq 1);
@@ -254,14 +254,14 @@
 by (blast_tac (claset() addSEs [less_irrefl, less_SucE] addEs [less_asym]) 1);
 qed "Suc_lessI";
 
-val [prem] = goal thy "Suc(m) < n ==> m<n";
-by (rtac (prem RS rev_mp) 1);
+Goal "Suc(m) < n ==> m<n";
+by (etac rev_mp 1);
 by (nat_ind_tac "n" 1);
 by (ALLGOALS (fast_tac (claset() addSIs [lessI RS less_SucI]
                                  addEs  [less_trans, lessE])));
 qed "Suc_lessD";
 
-val [major,minor] = goal thy 
+val [major,minor] = Goal 
     "[| Suc(i)<k;  !!j. [| i<j;  k=Suc(j) |] ==> P \
 \    |] ==> P";
 by (rtac (major RS lessE) 1);
@@ -299,7 +299,7 @@
 qed "not_less_eq";
 
 (*Complete induction, aka course-of-values induction*)
-val prems = goalw thy [less_def]
+val prems = Goalw [less_def]
     "[| !!n. [| ! m::nat. m<n --> P(m) |] ==> P(n) |]  ==>  P(n)";
 by (wf_ind_tac "n" [wf_pred_nat RS wf_trancl] 1);
 by (eresolve_tac prems 1);
@@ -350,12 +350,12 @@
 but less_Suc_eq makes additional problems with terms of the form 0 < Suc (...)
 *)
 
-val prems = goalw thy [le_def] "~n<m ==> m<=(n::nat)";
-by (resolve_tac prems 1);
+Goalw [le_def] "~n<m ==> m<=(n::nat)";
+by (assume_tac 1);
 qed "leI";
 
-val prems = goalw thy [le_def] "m<=n ==> ~ n < (m::nat)";
-by (resolve_tac prems 1);
+Goalw [le_def] "m<=n ==> ~ n < (m::nat)";
+by (assume_tac 1);
 qed "leD";
 
 val leE = make_elim leD;
@@ -505,7 +505,7 @@
 by (simp_tac (simpset() addsimps [lemma]) 1);
 qed "Least_nat_def";
 
-val [prem1,prem2] = goalw thy [Least_nat_def]
+val [prem1,prem2] = Goalw [Least_nat_def]
     "[| P(k::nat);  !!x. x<k ==> ~P(x) |] ==> (LEAST x. P(x)) = k";
 by (rtac select_equality 1);
 by (blast_tac (claset() addSIs [prem1,prem2]) 1);
@@ -513,8 +513,8 @@
 by (blast_tac (claset() addSIs [prem1] addSDs [prem2]) 1);
 qed "Least_equality";
 
-val [prem] = goal thy "P(k::nat) ==> P(LEAST x. P(x))";
-by (rtac (prem RS rev_mp) 1);
+Goal "P(k::nat) ==> P(LEAST x. P(x))";
+by (etac rev_mp 1);
 by (res_inst_tac [("n","k")] less_induct 1);
 by (rtac impI 1);
 by (rtac classical 1);
@@ -525,8 +525,8 @@
 qed "LeastI";
 
 (*Proof is almost identical to the one above!*)
-val [prem] = goal thy "P(k::nat) ==> (LEAST x. P(x)) <= k";
-by (rtac (prem RS rev_mp) 1);
+Goal "P(k::nat) ==> (LEAST x. P(x)) <= k";
+by (etac rev_mp 1);
 by (res_inst_tac [("n","k")] less_induct 1);
 by (rtac impI 1);
 by (rtac classical 1);
@@ -536,10 +536,9 @@
 by (blast_tac (claset() addIs [less_imp_le,le_trans]) 1);
 qed "Least_le";
 
-val [prem] = goal thy "k < (LEAST x. P(x)) ==> ~P(k::nat)";
+Goal "k < (LEAST x. P(x)) ==> ~P(k::nat)";
 by (rtac notI 1);
-by (etac (rewrite_rule [le_def] Least_le RS notE) 1);
-by (rtac prem 1);
+by (etac (rewrite_rule [le_def] Least_le RS notE) 1 THEN assume_tac 1);
 qed "not_less_Least";
 
 (*** Instantiation of transitivity prover ***)
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Ord.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -8,15 +8,13 @@
 
 (** mono **)
 
-val [prem] = goalw Ord.thy [mono_def]
+val [prem] = Goalw [mono_def]
     "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
 by (REPEAT (ares_tac [allI, impI, prem] 1));
 qed "monoI";
 
-val [major,minor] = goalw Ord.thy [mono_def]
-    "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
-by (rtac (major RS spec RS spec RS mp) 1);
-by (rtac minor 1);
+Goalw [mono_def] "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
+by (Fast_tac 1);
 qed "monoD";
 
 
@@ -46,7 +44,7 @@
 by (simp_tac (simpset() addsimps prems) 1);
 qed "min_leastL";
 
-val prems = goalw thy [min_def]
+val prems = Goalw [min_def]
  "(!!x::'a::order. least <= x) ==> min x least = least";
 by (cut_facts_tac prems 1);
 by (Asm_simp_tac 1);
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Prod.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -24,7 +24,7 @@
 by (etac Abs_Prod_inverse 1);
 qed "inj_on_Abs_Prod";
 
-val prems = goalw Prod.thy [Pair_def]
+val prems = Goalw [Pair_def]
     "[| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R";
 by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1);
 by (REPEAT (ares_tac (prems@[ProdI]) 1));
@@ -49,7 +49,7 @@
            rtac (Rep_Prod_inverse RS sym RS trans),  etac arg_cong]);
 qed "PairE_lemma";
 
-val [prem] = goal Prod.thy "[| !!x y. p = (x,y) ==> Q |] ==> Q";
+val [prem] = Goal "[| !!x y. p = (x,y) ==> Q |] ==> Q";
 by (rtac (PairE_lemma RS exE) 1);
 by (REPEAT (eresolve_tac [prem,exE] 1));
 qed "PairE";
@@ -222,7 +222,7 @@
 by (Asm_simp_tac 1);
 qed "splitI";
 
-val prems = goalw Prod.thy [split_def]
+val prems = Goalw [split_def]
     "[| split c p;  !!x y. [| p = (x,y);  c x y |] ==> Q |] ==> Q";
 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
 qed "splitE";
@@ -246,7 +246,7 @@
 by (Asm_simp_tac 1);
 qed "mem_splitI2";
 
-val prems = goalw Prod.thy [split_def]
+val prems = Goalw [split_def]
     "[| z: split c p;  !!x y. [| p = (x,y);  z: c x y |] ==> Q |] ==> Q";
 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
 qed "mem_splitE";
@@ -298,13 +298,13 @@
 qed "prod_fun_ident";
 Addsimps [prod_fun_ident];
 
-val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
+Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
 by (rtac image_eqI 1);
 by (rtac (prod_fun RS sym) 1);
-by (resolve_tac prems 1);
+by (assume_tac 1);
 qed "prod_fun_imageI";
 
-val major::prems = goal Prod.thy
+val major::prems = Goal
     "[| c: (prod_fun f g)``r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
 \    |] ==> P";
 by (rtac (major RS imageE) 1);
@@ -354,7 +354,7 @@
 
 AddSEs [SigmaE2, SigmaE];
 
-val prems = goal Prod.thy
+val prems = Goal
     "[| A<=C;  !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
 by (cut_facts_tac prems 1);
 by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
@@ -384,14 +384,14 @@
 
 (*** Domain of a relation ***)
 
-val prems = goalw Prod.thy [image_def] "(a,b) : r ==> a : fst``r";
+Goalw [image_def] "(a,b) : r ==> a : fst``r";
 by (rtac CollectI 1);
 by (rtac bexI 1);
 by (rtac (fst_conv RS sym) 1);
-by (resolve_tac prems 1);
+by (assume_tac 1);
 qed "fst_imageI";
 
-val major::prems = goal Prod.thy
+val major::prems = Goal
     "[| a : fst``r;  !!y.[| (a,y) : r |] ==> P |] ==> P"; 
 by (rtac (major RS imageE) 1);
 by (resolve_tac prems 1);
@@ -402,15 +402,14 @@
 
 (*** Range of a relation ***)
 
-val prems = goalw Prod.thy [image_def] "(a,b) : r ==> b : snd``r";
+Goalw [image_def] "(a,b) : r ==> b : snd``r";
 by (rtac CollectI 1);
 by (rtac bexI 1);
 by (rtac (snd_conv RS sym) 1);
-by (resolve_tac prems 1);
+by (assume_tac 1);
 qed "snd_imageI";
 
-val major::prems = goal Prod.thy
-    "[| a : snd``r;  !!y.[| (y,a) : r |] ==> P |] ==> P"; 
+val major::prems = Goal "[| a : snd``r;  !!y.[| (y,a) : r |] ==> P |] ==> P"; 
 by (rtac (major RS imageE) 1);
 by (resolve_tac prems 1);
 by (etac ssubst 1);
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/RelPow.ML
--- a/src/HOL/RelPow.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/RelPow.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -31,14 +31,14 @@
 by (Asm_full_simp_tac 1);
 qed "rel_pow_0_E";
 
-val [major,minor] = goal RelPow.thy
+val [major,minor] = Goal
   "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
 by (cut_facts_tac [major] 1);
 by (Asm_full_simp_tac  1);
 by (blast_tac (claset() addIs [minor]) 1);
 qed "rel_pow_Suc_E";
 
-val [p1,p2,p3] = goal RelPow.thy
+val [p1,p2,p3] = Goal
     "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
 \       !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P  \
 \    |] ==> P";
@@ -52,18 +52,20 @@
 
 Goal "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
 by (nat_ind_tac "n" 1);
-by (blast_tac (claset() addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
-by (blast_tac (claset() addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
+by (blast_tac (claset() addIs [rel_pow_0_I] 
+	                addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
+by (blast_tac (claset() addIs [rel_pow_Suc_I]  
+	                addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
 qed_spec_mp "rel_pow_Suc_D2";
 
 
 Goal "!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)";
 by (nat_ind_tac "n" 1);
-by (fast_tac (claset() addss (simpset())) 1);
-by (fast_tac (claset() addss (simpset())) 1);
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1);
 qed_spec_mp "rel_pow_Suc_D2'";
 
-val [p1,p2,p3] = goal RelPow.thy
+val [p1,p2,p3] = Goal
     "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
 \       !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P  \
 \    |] ==> P";
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Relation.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -12,7 +12,7 @@
 by (Blast_tac 1);
 qed "idI";
 
-val major::prems = goalw thy [id_def]
+val major::prems = Goalw [id_def]
     "[| p: id;  !!x.[| p = (x,x) |] ==> P  \
 \    |] ==>  P";  
 by (rtac (major RS CollectE) 1);
@@ -34,7 +34,7 @@
 qed "compI";
 
 (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
-val prems = goalw thy [comp_def]
+val prems = Goalw [comp_def]
     "[| xz : r O s;  \
 \       !!x y z. [| xz = (x,z);  (x,y):s;  (y,z):r |] ==> P \
 \    |] ==> P";
@@ -43,7 +43,7 @@
      ORELSE ares_tac prems 1));
 qed "compE";
 
-val prems = goal thy
+val prems = Goal
     "[| (a,c) : r O s;  \
 \       !!y. [| (a,y):s;  (y,c):r |] ==> P \
 \    |] ==> P";
@@ -78,7 +78,7 @@
 
 (** Natural deduction for trans(r) **)
 
-val prems = goalw thy [trans_def]
+val prems = Goalw [trans_def]
     "(!! x y z. [| (x,y):r;  (y,z):r |] ==> (x,z):r) ==> trans(r)";
 by (REPEAT (ares_tac (prems@[allI,impI]) 1));
 qed "transI";
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Set.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -17,17 +17,17 @@
 by (Asm_simp_tac 1);
 qed "CollectI";
 
-val prems = goal Set.thy "!!a. a : {x. P(x)} ==> P(a)";
+Goal "a : {x. P(x)} ==> P(a)";
 by (Asm_full_simp_tac 1);
 qed "CollectD";
 
-val [prem] = goal Set.thy "[| !!x. (x:A) = (x:B) |] ==> A = B";
+val [prem] = Goal "[| !!x. (x:A) = (x:B) |] ==> A = B";
 by (rtac (prem RS ext RS arg_cong RS box_equals) 1);
 by (rtac Collect_mem_eq 1);
 by (rtac Collect_mem_eq 1);
 qed "set_ext";
 
-val [prem] = goal Set.thy "[| !!x. P(x)=Q(x) |] ==> {x. P(x)} = {x. Q(x)}";
+val [prem] = Goal "[| !!x. P(x)=Q(x) |] ==> {x. P(x)} = {x. Q(x)}";
 by (rtac (prem RS ext RS arg_cong) 1);
 qed "Collect_cong";
 
@@ -39,17 +39,16 @@
 
 section "Bounded quantifiers";
 
-val prems = goalw Set.thy [Ball_def]
+val prems = Goalw [Ball_def]
     "[| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)";
 by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
 qed "ballI";
 
-val [major,minor] = goalw Set.thy [Ball_def]
-    "[| ! x:A. P(x);  x:A |] ==> P(x)";
-by (rtac (minor RS (major RS spec RS mp)) 1);
+Goalw [Ball_def] "[| ! x:A. P(x);  x:A |] ==> P(x)";
+by (Blast_tac 1);
 qed "bspec";
 
-val major::prems = goalw Set.thy [Ball_def]
+val major::prems = Goalw [Ball_def]
     "[| ! x:A. P(x);  P(x) ==> Q;  x~:A ==> Q |] ==> Q";
 by (rtac (major RS spec RS impCE) 1);
 by (REPEAT (eresolve_tac prems 1));
@@ -61,9 +60,8 @@
 AddSIs [ballI];
 AddEs  [ballE];
 
-val prems = goalw Set.thy [Bex_def]
-    "[| P(x);  x:A |] ==> ? x:A. P(x)";
-by (REPEAT (ares_tac (prems @ [exI,conjI]) 1));
+Goalw [Bex_def] "[| P(x);  x:A |] ==> ? x:A. P(x)";
+by (Blast_tac 1);
 qed "bexI";
 
 qed_goal "bexCI" Set.thy 
@@ -72,7 +70,7 @@
   [ (rtac classical 1),
     (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1))  ]);
 
-val major::prems = goalw Set.thy [Bex_def]
+val major::prems = Goalw [Bex_def]
     "[| ? x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q  |] ==> Q";
 by (rtac (major RS exE) 1);
 by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1));
@@ -95,7 +93,7 @@
 
 (** Congruence rules **)
 
-val prems = goal Set.thy
+val prems = Goal
     "[| A=B;  !!x. x:B ==> P(x) = Q(x) |] ==> \
 \    (! x:A. P(x)) = (! x:B. Q(x))";
 by (resolve_tac (prems RL [ssubst]) 1);
@@ -103,7 +101,7 @@
      ORELSE eresolve_tac ([make_elim bspec, mp] @ (prems RL [iffE])) 1));
 qed "ball_cong";
 
-val prems = goal Set.thy
+val prems = Goal
     "[| A=B;  !!x. x:B ==> P(x) = Q(x) |] ==> \
 \    (? x:A. P(x)) = (? x:B. Q(x))";
 by (resolve_tac (prems RL [ssubst]) 1);
@@ -113,7 +111,7 @@
 
 section "Subsets";
 
-val prems = goalw Set.thy [subset_def] "(!!x. x:A ==> x:B) ==> A <= B";
+val prems = Goalw [subset_def] "(!!x. x:A ==> x:B) ==> A <= B";
 by (REPEAT (ares_tac (prems @ [ballI]) 1));
 qed "subsetI";
 
@@ -130,9 +128,8 @@
 Blast.overloaded ("op ``", domain_type o domain_type);
 
 (*Rule in Modus Ponens style*)
-val major::prems = goalw Set.thy [subset_def] "[| A <= B;  c:A |] ==> c:B";
-by (rtac (major RS bspec) 1);
-by (resolve_tac prems 1);
+Goalw [subset_def] "[| A <= B;  c:A |] ==> c:B";
+by (Blast_tac 1);
 qed "subsetD";
 
 (*The same, with reversed premises for use with etac -- cf rev_mp*)
@@ -149,7 +146,7 @@
  (fn prems=>  [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]);
 
 (*Classical elimination rule*)
-val major::prems = goalw Set.thy [subset_def] 
+val major::prems = Goalw [subset_def] 
     "[| A <= B;  c~:A ==> P;  c:B ==> P |] ==> P";
 by (rtac (major RS ballE) 1);
 by (REPEAT (eresolve_tac prems 1));
@@ -164,7 +161,7 @@
 qed_goal "subset_refl" Set.thy "A <= (A::'a set)"
  (fn _=> [Fast_tac 1]);		(*Blast_tac would try order_refl and fail*)
 
-val prems = goal Set.thy "!!B. [| A<=B;  B<=C |] ==> A<=(C::'a set)";
+Goal "[| A<=B;  B<=C |] ==> A<=(C::'a set)";
 by (Blast_tac 1);
 qed "subset_trans";
 
@@ -172,32 +169,32 @@
 section "Equality";
 
 (*Anti-symmetry of the subset relation*)
-val prems = goal Set.thy "[| A <= B;  B <= A |] ==> A = (B::'a set)";
-by (rtac (iffI RS set_ext) 1);
-by (REPEAT (ares_tac (prems RL [subsetD]) 1));
+Goal "[| A <= B;  B <= A |] ==> A = (B::'a set)";
+br set_ext 1;
+by (blast_tac (claset() addIs [subsetD]) 1);
 qed "subset_antisym";
 val equalityI = subset_antisym;
 
 AddSIs [equalityI];
 
 (* Equality rules from ZF set theory -- are they appropriate here? *)
-val prems = goal Set.thy "A = B ==> A<=(B::'a set)";
-by (resolve_tac (prems RL [subst]) 1);
+Goal "A = B ==> A<=(B::'a set)";
+by (etac ssubst 1);
 by (rtac subset_refl 1);
 qed "equalityD1";
 
-val prems = goal Set.thy "A = B ==> B<=(A::'a set)";
-by (resolve_tac (prems RL [subst]) 1);
+Goal "A = B ==> B<=(A::'a set)";
+by (etac ssubst 1);
 by (rtac subset_refl 1);
 qed "equalityD2";
 
-val prems = goal Set.thy
+val prems = Goal
     "[| A = B;  [| A<=B; B<=(A::'a set) |] ==> P |]  ==>  P";
 by (resolve_tac prems 1);
 by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
 qed "equalityE";
 
-val major::prems = goal Set.thy
+val major::prems = Goal
     "[| A = B;  [| c:A; c:B |] ==> P;  [| c~:A; c~:B |] ==> P |]  ==>  P";
 by (rtac (major RS equalityE) 1);
 by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1));
@@ -206,7 +203,7 @@
 (*Lemma for creating induction formulae -- for "pattern matching" on p
   To make the induction hypotheses usable, apply "spec" or "bspec" to
   put universal quantifiers over the free variables in p. *)
-val prems = goal Set.thy 
+val prems = Goal 
     "[| p:A;  !!z. z:A ==> p=z --> R |] ==> R";
 by (rtac mp 1);
 by (REPEAT (resolve_tac (refl::prems) 1));
@@ -305,17 +302,15 @@
 
 Addsimps [Compl_iff];
 
-val prems = goalw Set.thy [Compl_def]
-    "[| c:A ==> False |] ==> c : Compl(A)";
+val prems = Goalw [Compl_def] "[| c:A ==> False |] ==> c : Compl(A)";
 by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1));
 qed "ComplI";
 
 (*This form, with negated conclusion, works well with the Classical prover.
   Negated assumptions behave like formulae on the right side of the notional
   turnstile...*)
-val major::prems = goalw Set.thy [Compl_def]
-    "c : Compl(A) ==> c~:A";
-by (rtac (major RS CollectD) 1);
+Goalw [Compl_def] "c : Compl(A) ==> c~:A";
+by (etac CollectD 1);
 qed "ComplD";
 
 val ComplE = make_elim ComplD;
@@ -345,7 +340,7 @@
   [ (Simp_tac 1),
     (REPEAT (ares_tac (prems@[disjCI]) 1)) ]);
 
-val major::prems = goalw Set.thy [Un_def]
+val major::prems = Goalw [Un_def]
     "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P";
 by (rtac (major RS CollectD RS disjE) 1);
 by (REPEAT (eresolve_tac prems 1));
@@ -374,7 +369,7 @@
 by (Asm_full_simp_tac 1);
 qed "IntD2";
 
-val [major,minor] = goal Set.thy
+val [major,minor] = Goal
     "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P";
 by (rtac minor 1);
 by (rtac (major RS IntD1) 1);
@@ -479,7 +474,7 @@
 by Auto_tac;
 qed "UN_I";
 
-val major::prems = goalw Set.thy [UNION_def]
+val major::prems = Goalw [UNION_def]
     "[| b : (UN x:A. B(x));  !!x.[| x:A;  b: B(x) |] ==> R |] ==> R";
 by (rtac (major RS CollectD RS bexE) 1);
 by (REPEAT (ares_tac prems 1));
@@ -488,7 +483,7 @@
 AddIs  [UN_I];
 AddSEs [UN_E];
 
-val prems = goal Set.thy
+val prems = Goal
     "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==> \
 \    (UN x:A. C(x)) = (UN x:B. D(x))";
 by (REPEAT (etac UN_E 1
@@ -505,7 +500,7 @@
 
 Addsimps [INT_iff];
 
-val prems = goalw Set.thy [INTER_def]
+val prems = Goalw [INTER_def]
     "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))";
 by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1));
 qed "INT_I";
@@ -515,7 +510,7 @@
 qed "INT_D";
 
 (*"Classical" elimination -- by the Excluded Middle on a:A *)
-val major::prems = goalw Set.thy [INTER_def]
+val major::prems = Goalw [INTER_def]
     "[| b : (INT x:A. B(x));  b: B(a) ==> R;  a~:A ==> R |] ==> R";
 by (rtac (major RS CollectD RS ballE) 1);
 by (REPEAT (eresolve_tac prems 1));
@@ -524,7 +519,7 @@
 AddSIs [INT_I];
 AddEs  [INT_D, INT_E];
 
-val prems = goal Set.thy
+val prems = Goal
     "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==> \
 \    (INT x:A. C(x)) = (INT x:B. D(x))";
 by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI]));
@@ -546,7 +541,7 @@
 by Auto_tac;
 qed "UnionI";
 
-val major::prems = goalw Set.thy [Union_def]
+val major::prems = Goalw [Union_def]
     "[| A : Union(C);  !!X.[| A:X;  X:C |] ==> R |] ==> R";
 by (rtac (major RS UN_E) 1);
 by (REPEAT (ares_tac prems 1));
@@ -564,7 +559,7 @@
 
 Addsimps [Inter_iff];
 
-val prems = goalw Set.thy [Inter_def]
+val prems = Goalw [Inter_def]
     "[| !!X. X:C ==> A:X |] ==> A : Inter(C)";
 by (REPEAT (ares_tac ([INT_I] @ prems) 1));
 qed "InterI";
@@ -576,7 +571,7 @@
 qed "InterD";
 
 (*"Classical" elimination rule -- does not require proving X:C *)
-val major::prems = goalw Set.thy [Inter_def]
+val major::prems = Goalw [Inter_def]
     "[| A : Inter(C);  X~:C ==> R;  A:X ==> R |] ==> R";
 by (rtac (major RS INT_E) 1);
 by (REPEAT (eresolve_tac prems 1));
@@ -589,15 +584,15 @@
 (*** Image of a set under a function ***)
 
 (*Frequently b does not have the syntactic form of f(x).*)
-val prems = goalw thy [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
-by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1));
+Goalw [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
+by (Blast_tac 1);
 qed "image_eqI";
 Addsimps [image_eqI];
 
 bind_thm ("imageI", refl RS image_eqI);
 
 (*The eta-expansion gives variable-name preservation.*)
-val major::prems = goalw thy [image_def]
+val major::prems = Goalw [image_def]
     "[| b : (%x. f(x))``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P"; 
 by (rtac (major RS CollectD RS bexE) 1);
 by (REPEAT (ares_tac prems 1));
@@ -621,7 +616,7 @@
 
 (*Replaces the three steps subsetI, imageE, hyp_subst_tac, but breaks too
   many existing proofs.*)
-val prems = goal thy "(!!x. x:A ==> f(x) : B) ==> f``A <= B";
+val prems = Goal "(!!x. x:A ==> f(x) : B) ==> f``A <= B";
 by (blast_tac (claset() addIs prems) 1);
 qed "image_subsetI";
 
@@ -634,7 +629,7 @@
 
 bind_thm ("rangeI", UNIV_I RS imageI);
 
-val [major,minor] = goal thy 
+val [major,minor] = Goal 
     "[| b : range(%x. f(x));  !!x. b=f(x) ==> P |] ==> P"; 
 by (rtac (major RS imageE) 1);
 by (etac minor 1);
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/Sum.ML
--- a/src/HOL/Sum.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Sum.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-For Sum.thy.  The disjoint sum of two types
+The disjoint sum of two types
 *)
 
 open Sum;
@@ -51,13 +51,13 @@
 
 (** Injectiveness of Inl and Inr **)
 
-val [major] = goalw Sum.thy [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
-by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
+Goalw [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
+by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1);
 by (Blast_tac 1);
 qed "Inl_Rep_inject";
 
-val [major] = goalw Sum.thy [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
-by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
+Goalw [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
+by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1);
 by (Blast_tac 1);
 qed "Inr_Rep_inject";
 
@@ -101,7 +101,7 @@
 
 (** Elimination rules **)
 
-val major::prems = goalw Sum.thy [sum_def]
+val major::prems = Goalw [sum_def]
     "[| u: A Plus B;  \
 \       !!x. [| x:A;  u=Inl(x) |] ==> P; \
 \       !!y. [| y:B;  u=Inr(y) |] ==> P \
@@ -130,7 +130,7 @@
 
 (** Exhaustion rule for sums -- a degenerate form of induction **)
 
-val prems = goalw Sum.thy [Inl_def,Inr_def]
+val prems = Goalw [Inl_def,Inr_def]
     "[| !!x::'a. s = Inl(x) ==> P;  !!y::'b. s = Inr(y) ==> P \
 \    |] ==> P";
 by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1);
@@ -140,7 +140,7 @@
                     rtac (Rep_Sum_inverse RS sym)]));
 qed "sumE";
 
-val prems = goal thy "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x";
+val prems = Goal "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x";
 by (res_inst_tac [("s","x")] sumE 1);
 by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems)));
 qed "sum_induct";
@@ -177,7 +177,7 @@
 
 val PartI = refl RSN (2,Part_eqI);
 
-val major::prems = goalw Sum.thy [Part_def]
+val major::prems = Goalw [Part_def]
     "[| a : Part A h;  !!z. [| a : A;  a=h(z) |] ==> P  \
 \    |] ==> P";
 by (rtac (major RS IntE) 1);
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Trancl.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-For Trancl.thy.  Theorems about the transitive closure of a relation
+Theorems about the transitive closure of a relation
 *)
 
 open Trancl;
@@ -46,7 +46,7 @@
 
 (** standard induction rule **)
 
-val major::prems = goal Trancl.thy 
+val major::prems = Goal 
   "[| (a,b) : r^*; \
 \     !!x. P((x,x)); \
 \     !!x y z.[| P((x,y)); (x,y): r^*; (y,z): r |]  ==>  P((x,z)) |] \
@@ -56,7 +56,7 @@
 qed "rtrancl_full_induct";
 
 (*nice induction rule*)
-val major::prems = goal Trancl.thy
+val major::prems = Goal
     "[| (a::'a,b) : r^*;    \
 \       P(a); \
 \       !!y z.[| (a,y) : r^*;  (y,z) : r;  P(y) |] ==> P(z) |]  \
@@ -85,7 +85,7 @@
 
 
 (*elimination of rtrancl -- by induction on a special formula*)
-val major::prems = goal Trancl.thy
+val major::prems = Goal
     "[| (a::'a,b) : r^*;  (a = b) ==> P;        \
 \       !!y.[| (a,y) : r^*; (y,b) : r |] ==> P  \
 \    |] ==> P";
@@ -133,8 +133,9 @@
 qed "rtrancl_subset";
 
 Goal "(R^* Un S^*)^* = (R Un S)^*";
-by (blast_tac (claset() addSIs [rtrancl_subset]
-                       addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
+(*Blast_tac: PROOF FAILED*)
+by (Blast.depth_tac (claset() addSIs [rtrancl_subset]
+                       addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 4 1);
 qed "rtrancl_Un_rtrancl";
 
 Goal "(R^=)^* = R^*";
@@ -160,7 +161,7 @@
 by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]));
 qed "rtrancl_converse";
 
-val major::prems = goal Trancl.thy
+val major::prems = Goal
     "[| (a,b) : r^*; P(b); \
 \       !!y z.[| (y,z) : r;  (z,b) : r^*;  P(z) |] ==> P(y) |]  \
 \     ==> P(a)";
@@ -169,7 +170,7 @@
 by (blast_tac (claset() addIs prems addSDs[rtrancl_converseD])1);
 qed "converse_rtrancl_induct";
 
-val prems = goal Trancl.thy
+val prems = Goal
  "[| ((a,b),(c,d)) : r^*; P c d; \
 \    !!x y z u.[| ((x,y),(z,u)) : r;  ((z,u),(c,d)) : r^*;  P z u |] ==> P x y\
 \ |] ==> P a b";
@@ -183,7 +184,7 @@
 by (REPEAT(ares_tac prems 1));
 qed "converse_rtrancl_induct2";
 
-val major::prems = goal Trancl.thy
+val major::prems = Goal
  "[| (x,z):r^*; \
 \    x=z ==> P; \
 \    !!y. [| (x,y):r; (y,z):r^* |] ==> P \
@@ -237,7 +238,7 @@
 qed "rtrancl_into_trancl2";
 
 (*Nice induction rule for trancl*)
-val major::prems = goal Trancl.thy
+val major::prems = Goal
   "[| (a,b) : r^+;                                      \
 \     !!y.  [| (a,y) : r |] ==> P(y);                   \
 \     !!y z.[| (a,y) : r^+;  (y,z) : r;  P(y) |] ==> P(z)       \
@@ -252,7 +253,7 @@
 qed "trancl_induct";
 
 (*elimination of r^+ -- NOT an induction rule*)
-val major::prems = goal Trancl.thy
+val major::prems = Goal
     "[| (a::'a,b) : r^+;  \
 \       (a,b) : r ==> P; \
 \       !!y.[| (a,y) : r^+;  (y,b) : r |] ==> P  \
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Univ.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -14,7 +14,7 @@
 by (rtac split 1);
 qed "apfst_conv";
 
-val [major,minor] = goal Univ.thy
+val [major,minor] = Goal
     "[| q = apfst f p;  !!x y. [| p = (x,y);  q = (f(x),y) |] ==> R \
 \    |] ==> R";
 by (rtac PairE 1);
@@ -27,26 +27,27 @@
 
 (** Push -- an injection, analogous to Cons on lists **)
 
-val [major] = goalw Univ.thy [Push_def] "Push i f = Push j g  ==> i=j";
-by (rtac (major RS fun_cong RS box_equals RS Suc_inject) 1);
+Goalw [Push_def] "Push i f = Push j g  ==> i=j";
+by (etac (fun_cong RS box_equals RS Suc_inject) 1);
 by (rtac nat_case_0 1);
 by (rtac nat_case_0 1);
 qed "Push_inject1";
 
-val [major] = goalw Univ.thy [Push_def] "Push i f = Push j g  ==> f=g";
-by (rtac (major RS fun_cong RS ext RS box_equals) 1);
+Goalw [Push_def] "Push i f = Push j g  ==> f=g";
+by (rtac (ext RS box_equals) 1);
+by (etac fun_cong 1);
 by (rtac (nat_case_Suc RS ext) 1);
 by (rtac (nat_case_Suc RS ext) 1);
 qed "Push_inject2";
 
-val [major,minor] = goal Univ.thy
+val [major,minor] = Goal
     "[| Push i f =Push j g;  [| i=j;  f=g |] ==> P \
 \    |] ==> P";
 by (rtac ((major RS Push_inject2) RS ((major RS Push_inject1) RS minor)) 1);
 qed "Push_inject";
 
-val [major] = goalw Univ.thy [Push_def] "Push k f =(%z.0) ==> P";
-by (rtac (major RS fun_cong RS box_equals RS Suc_neq_Zero) 1);
+Goalw [Push_def] "Push k f =(%z.0) ==> P";
+by (etac (fun_cong RS box_equals RS Suc_neq_Zero) 1);
 by (rtac nat_case_0 1);
 by (rtac refl 1);
 qed "Push_neq_K0";
@@ -125,7 +126,7 @@
 
 (** Injectiveness of Push_Node **)
 
-val [major,minor] = goalw Univ.thy [Push_Node_def]
+val [major,minor] = Goalw [Push_Node_def]
     "[| Push_Node i m =Push_Node j n;  [| i=j;  m=n |] ==> P \
 \    |] ==> P";
 by (rtac (major RS Abs_Node_inject RS apfst_convE) 1);
@@ -150,17 +151,17 @@
 by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
 qed "Scons_inject_lemma2";
 
-val [major] = goal Univ.thy "Scons M N = Scons M' N' ==> M=M'";
-by (rtac (major RS equalityE) 1);
+Goal "Scons M N = Scons M' N' ==> M=M'";
+by (etac equalityE 1);
 by (REPEAT (ares_tac [equalityI, Scons_inject_lemma1] 1));
 qed "Scons_inject1";
 
-val [major] = goal Univ.thy "Scons M N = Scons M' N' ==> N=N'";
-by (rtac (major RS equalityE) 1);
+Goal "Scons M N = Scons M' N' ==> N=N'";
+by (etac equalityE 1);
 by (REPEAT (ares_tac [equalityI, Scons_inject_lemma2] 1));
 qed "Scons_inject2";
 
-val [major,minor] = goal Univ.thy
+val [major,minor] = Goal
     "[| Scons M N = Scons M' N';  [| M=M';  N=N' |] ==> P \
 \    |] ==> P";
 by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1);
@@ -302,7 +303,7 @@
 qed "uprodI";
 
 (*The general elimination rule*)
-val major::prems = goalw Univ.thy [uprod_def]
+val major::prems = Goalw [uprod_def]
     "[| c : A<*>B;  \
 \       !!x y. [| x:A;  y:B;  c = Scons x y |] ==> P \
 \    |] ==> P";
@@ -312,7 +313,7 @@
 qed "uprodE";
 
 (*Elimination of a pair -- introduces no eigenvariables*)
-val prems = goal Univ.thy
+val prems = Goal
     "[| Scons M N : A<*>B;      [| M:A;  N:B |] ==> P   \
 \    |] ==> P";
 by (rtac uprodE 1);
@@ -330,7 +331,7 @@
 by (Blast_tac 1);
 qed "usum_In1I";
 
-val major::prems = goalw Univ.thy [usum_def]
+val major::prems = Goalw [usum_def]
     "[| u : A<+>B;  \
 \       !!x. [| x:A;  u=In0(x) |] ==> P; \
 \       !!y. [| y:B;  u=In1(y) |] ==> P \
@@ -352,12 +353,12 @@
 
 AddIffs [In0_not_In1, In1_not_In0];
 
-val [major] = goalw Univ.thy [In0_def] "In0(M) = In0(N) ==>  M=N";
-by (rtac (major RS Scons_inject2) 1);
+Goalw [In0_def] "In0(M) = In0(N) ==>  M=N";
+by (etac (Scons_inject2) 1);
 qed "In0_inject";
 
-val [major] = goalw Univ.thy [In1_def] "In1(M) = In1(N) ==>  M=N";
-by (rtac (major RS Scons_inject2) 1);
+Goalw [In1_def] "In1(M) = In1(N) ==>  M=N";
+by (etac (Scons_inject2) 1);
 qed "In1_inject";
 
 Goal "(In0 M = In0 N) = (M=N)";
@@ -385,14 +386,13 @@
 by (Blast_tac 1);
 qed "ntrunc_subsetI";
 
-val [major] = goalw Univ.thy [ntrunc_def]
-    "(!!k. ntrunc k M <= N) ==> M<=N";
+val [major] = Goalw [ntrunc_def] "(!!k. ntrunc k M <= N) ==> M<=N";
 by (blast_tac (claset() addIs [less_add_Suc1, less_add_Suc2, 
 			       major RS subsetD]) 1);
 qed "ntrunc_subsetD";
 
 (*A generalized form of the take-lemma*)
-val [major] = goal Univ.thy "(!!k. ntrunc k M = ntrunc k N) ==> M=N";
+val [major] = Goal "(!!k. ntrunc k M = ntrunc k N) ==> M=N";
 by (rtac equalityI 1);
 by (ALLGOALS (rtac ntrunc_subsetD));
 by (ALLGOALS (rtac (ntrunc_subsetI RSN (2, subset_trans))));
@@ -400,7 +400,7 @@
 by (rtac (major RS equalityD2) 1);
 qed "ntrunc_equality";
 
-val [major] = goalw Univ.thy [o_def]
+val [major] = Goalw [o_def]
     "[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2";
 by (rtac (ntrunc_equality RS ext) 1);
 by (rtac (major RS fun_cong) 1);
@@ -478,7 +478,7 @@
 val diagI = refl RS diag_eqI |> standard;
 
 (*The general elimination rule*)
-val major::prems = goalw Univ.thy [diag_def]
+val major::prems = Goalw [diag_def]
     "[| c : diag(A);  \
 \       !!x y. [| x:A;  c = (x,x) |] ==> P \
 \    |] ==> P";
@@ -494,7 +494,7 @@
 qed "dprodI";
 
 (*The general elimination rule*)
-val major::prems = goalw Univ.thy [dprod_def]
+val major::prems = Goalw [dprod_def]
     "[| c : r<**>s;  \
 \       !!x y x' y'. [| (x,x') : r;  (y,y') : s;  c = (Scons x y, Scons x' y') |] ==> P \
 \    |] ==> P";
@@ -514,7 +514,7 @@
 by (Blast_tac 1);
 qed "dsum_In1I";
 
-val major::prems = goalw Univ.thy [dsum_def]
+val major::prems = Goalw [dsum_def]
     "[| w : r<++>s;  \
 \       !!x x'. [| (x,x') : r;  w = (In0(x), In0(x')) |] ==> P; \
 \       !!y y'. [| (y,y') : s;  w = (In1(y), In1(y')) |] ==> P \
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/WF.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -12,7 +12,7 @@
 val H_cong1 = refl RS H_cong;
 
 (*Restriction to domain A.  If r is well-founded over A then wf(r)*)
-val [prem1,prem2] = goalw WF.thy [wf_def]
+val [prem1,prem2] = Goalw [wf_def]
  "[| r <= A Times A;  \
 \    !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x);  x:A |] ==> P(x) |]  \
 \ ==>  wf(r)";
@@ -22,7 +22,7 @@
 by (best_tac (claset() addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1);
 qed "wfI";
 
-val major::prems = goalw WF.thy [wf_def]
+val major::prems = Goalw [wf_def]
     "[| wf(r);          \
 \       !!x.[| ! y. (y,x): r --> P(y) |] ==> P(x) \
 \    |]  ==>  P(a)";
@@ -36,26 +36,25 @@
            rename_last_tac a ["1"] (i+1),
            ares_tac prems i];
 
-val prems = goal WF.thy "[| wf(r);  (a,x):r;  (x,a):r |] ==> P";
+Goal "[| wf(r);  (a,x):r;  (x,a):r |] ==> P";
 by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1);
-by (blast_tac (claset() addIs prems) 1);
-by (wf_ind_tac "a" prems 1);
+by (Blast_tac 1);
+by (wf_ind_tac "a" [] 1);
 by (Blast_tac 1);
 qed "wf_asym";
 
-val prems = goal WF.thy "[| wf(r);  (a,a): r |] ==> P";
-by (rtac wf_asym 1);
-by (REPEAT (resolve_tac prems 1));
+Goal "[| wf(r);  (a,a): r |] ==> P";
+by (blast_tac (claset() addEs [wf_asym]) 1);
 qed "wf_irrefl";
 
 (*transitive closure of a wf relation is wf! *)
-val [prem] = goal WF.thy "wf(r) ==> wf(r^+)";
-by (rewtac wf_def);
+Goal "wf(r) ==> wf(r^+)";
+by (stac wf_def 1);
 by (Clarify_tac 1);
 (*must retain the universal formula for later use!*)
 by (rtac allE 1 THEN assume_tac 1);
 by (etac mp 1);
-by (res_inst_tac [("a","x")] (prem RS wf_induct) 1);
+by (eres_inst_tac [("a","x")] wf_induct 1);
 by (rtac (impI RS allI) 1);
 by (etac tranclE 1);
 by (Blast_tac 1);
@@ -72,14 +71,13 @@
  * Minimal-element characterization of well-foundedness
  *---------------------------------------------------------------------------*)
 
-val wfr::_ = goalw WF.thy [wf_def]
-    "wf r ==> x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)";
-by (rtac (wfr RS spec RS mp RS spec) 1);
+Goalw [wf_def] "wf r ==> x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)";
+bd spec 1;
+by (etac (mp RS spec) 1);
 by (Blast_tac 1);
 val lemma1 = result();
 
-Goalw [wf_def]
-    "(! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)) ==> wf r";
+Goalw [wf_def] "(! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)) ==> wf r";
 by (Clarify_tac 1);
 by (dres_inst_tac [("x", "{x. ~ P x}")] spec 1);
 by (Blast_tac 1);
@@ -138,11 +136,10 @@
  * Wellfoundedness of `disjoint union'
  *---------------------------------------------------------------------------*)
 
-Goal
- "[| !i:I. wf(r i); \
-\    !i:I.!j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \
-\                              Domain(r j) Int Range(r i) = {} \
-\ |] ==> wf(UN i:I. r i)";
+Goal "[| !i:I. wf(r i); \
+\        !i:I.!j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \
+\                                  Domain(r j) Int Range(r i) = {} \
+\     |] ==> wf(UN i:I. r i)";
 by(asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
 by(Clarify_tac 1);
 by(rename_tac "A a" 1);
@@ -181,9 +178,8 @@
 by(Blast_tac 1);
 qed "wf_Union";
 
-Goal
- "[| wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \
-\ |] ==> wf(r Un s)";
+Goal "[| wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \
+\     |] ==> wf(r Un s)";
 br(simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1;
 by(Blast_tac 1);
 by(Blast_tac 1);
@@ -251,10 +247,9 @@
                         eresolve_tac [transD, mp, allE]));
 val wf_super_ss = HOL_ss addSolver indhyp_tac;
 
-val prems = goalw WF.thy [is_recfun_def,cut_def]
+Goalw [is_recfun_def,cut_def]
     "[| wf(r);  trans(r);  is_recfun r H a f;  is_recfun r H b g |] ==> \
     \ (x,a):r --> (x,b):r --> f(x)=g(x)";
-by (cut_facts_tac prems 1);
 by (etac wf_induct 1);
 by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
 by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1);
@@ -274,15 +269,13 @@
 
 (*** Main Existence Lemma -- Basic Properties of the_recfun ***)
 
-val prems = goalw WF.thy [the_recfun_def]
+Goalw [the_recfun_def]
     "is_recfun r H a f ==> is_recfun r H a (the_recfun r H a)";
-by (res_inst_tac [("P", "is_recfun r H a")] selectI 1);
-by (resolve_tac prems 1);
+by (eres_inst_tac [("P", "is_recfun r H a")] selectI 1);
 qed "is_the_recfun";
 
-val prems = goal WF.thy
- "!!r. [| wf(r);  trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
-by (wf_ind_tac "a" prems 1);
+Goal "[| wf(r);  trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
+by (wf_ind_tac "a" [] 1);
 by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
                  is_the_recfun 1);
 by (rewtac is_recfun_def);
@@ -309,7 +302,7 @@
 val unwind1_the_recfun = rewrite_rule[is_recfun_def] unfold_the_recfun;
 
 (*--------------Old proof-----------------------------------------------------
-val prems = goal WF.thy
+val prems = Goal
     "[| wf(r);  trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
 by (cut_facts_tac prems 1);
 by (wf_ind_tac "a" prems 1);
@@ -376,7 +369,7 @@
 (*---------------------------------------------------------------------------
  * This form avoids giant explosions in proofs.  NOTE USE OF == 
  *---------------------------------------------------------------------------*)
-val rew::prems = goal WF.thy
+val rew::prems = goal thy
     "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a";
 by (rewtac rew);
 by (REPEAT (resolve_tac (prems@[wfrec]) 1));
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/arith_data.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -56,7 +56,7 @@
 val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
 
 fun prove_conv expand_tac norm_tac sg (t, u) =
-  meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u)))
+  meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u)))
     (K [expand_tac, norm_tac]))
   handle ERROR => error ("The error(s) above occurred while trying to prove " ^
     (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/equalities.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -136,7 +136,7 @@
 qed "if_image_distrib";
 Addsimps[if_image_distrib];
 
-val prems= goal thy "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";
+val prems= Goal "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";
 by (rtac set_ext 1);
 by (simp_tac (simpset() addsimps image_def::prems) 1);
 qed "image_cong";
@@ -212,10 +212,6 @@
 by (Blast_tac 1);
 qed "Int_Un_distrib2";
 
-Goal "(A<=B) = (A Int B = A)";
-by (blast_tac (claset() addSEs [equalityCE]) 1);
-qed "subset_Int_eq";
-
 Goal "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
 by (blast_tac (claset() addEs [equalityCE]) 1);
 qed "Int_UNIV";
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/mono.ML
--- a/src/HOL/mono.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/mono.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -6,96 +6,96 @@
 Monotonicity of various operations
 *)
 
-goal Set.thy "!!A B. A<=B ==> f``A <= f``B";
+Goal "A<=B ==> f``A <= f``B";
 by (Blast_tac 1);
 qed "image_mono";
 
-goal Set.thy "!!A B. A<=B ==> Pow(A) <= Pow(B)";
+Goal "A<=B ==> Pow(A) <= Pow(B)";
 by (Blast_tac 1);
 qed "Pow_mono";
 
-goal Set.thy "!!A B. A<=B ==> Union(A) <= Union(B)";
+Goal "A<=B ==> Union(A) <= Union(B)";
 by (Blast_tac 1);
 qed "Union_mono";
 
-goal Set.thy "!!A B. B<=A ==> Inter(A) <= Inter(B)";
+Goal "B<=A ==> Inter(A) <= Inter(B)";
 by (Blast_tac 1);
 qed "Inter_anti_mono";
 
-val prems = goal Set.thy
+val prems = Goal
     "[| A<=B;  !!x. x:A ==> f(x)<=g(x) |] ==> \
 \    (UN x:A. f(x)) <= (UN x:B. g(x))";
 by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
 qed "UN_mono";
 
 (*The last inclusion is POSITIVE! *)
-val prems = goal Set.thy
+val prems = Goal
     "[| B<=A;  !!x. x:A ==> f(x)<=g(x) |] ==> \
 \    (INT x:A. f(x)) <= (INT x:A. g(x))";
 by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
 qed "INT_anti_mono";
 
-goal Set.thy "!!C D. C<=D ==> insert a C <= insert a D";
+Goal "C<=D ==> insert a C <= insert a D";
 by (Blast_tac 1);
 qed "insert_mono";
 
-goal Set.thy "!!A B. [| A<=C;  B<=D |] ==> A Un B <= C Un D";
+Goal "[| A<=C;  B<=D |] ==> A Un B <= C Un D";
 by (Blast_tac 1);
 qed "Un_mono";
 
-goal Set.thy "!!A B. [| A<=C;  B<=D |] ==> A Int B <= C Int D";
+Goal "[| A<=C;  B<=D |] ==> A Int B <= C Int D";
 by (Blast_tac 1);
 qed "Int_mono";
 
-goal Set.thy "!!A::'a set. [| A<=C;  D<=B |] ==> A-B <= C-D";
+Goal "!!A::'a set. [| A<=C;  D<=B |] ==> A-B <= C-D";
 by (Blast_tac 1);
 qed "Diff_mono";
 
-goal Set.thy "!!A B. A<=B ==> Compl(B) <= Compl(A)";
+Goal "A<=B ==> Compl(B) <= Compl(A)";
 by (Blast_tac 1);
 qed "Compl_anti_mono";
 
 (** Monotonicity of implications.  For inductive definitions **)
 
-goal Set.thy "!!A B x. A<=B ==> x:A --> x:B";
+Goal "A<=B ==> x:A --> x:B";
 by (rtac impI 1);
 by (etac subsetD 1);
 by (assume_tac 1);
 qed "in_mono";
 
-goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";
+Goal "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";
 by (Blast_tac 1);
 qed "conj_mono";
 
-goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)";
+Goal "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)";
 by (Blast_tac 1);
 qed "disj_mono";
 
-goal HOL.thy "!!P1 P2 Q1 Q2.[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)";
+Goal "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)";
 by (Blast_tac 1);
 qed "imp_mono";
 
-goal HOL.thy "P-->P";
+Goal "P-->P";
 by (rtac impI 1);
 by (assume_tac 1);
 qed "imp_refl";
 
-val [PQimp] = goal HOL.thy
+val [PQimp] = Goal
     "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))";
 by (blast_tac (claset() addIs [PQimp RS mp]) 1);
 qed "ex_mono";
 
-val [PQimp] = goal HOL.thy
+val [PQimp] = Goal
     "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))";
 by (blast_tac (claset() addIs [PQimp RS mp]) 1);
 qed "all_mono";
 
-val [PQimp] = goal Set.thy
+val [PQimp] = Goal
     "[| !!x. P(x) --> Q(x) |] ==> Collect(P) <= Collect(Q)";
 by (blast_tac (claset() addIs [PQimp RS mp]) 1);
 qed "Collect_mono";
 
-val [subs,PQimp] = goal Set.thy
+val [subs,PQimp] = Goal
     "[| A<=B;  !!x. x:A ==> P(x) --> Q(x) \
 \    |] ==> A Int Collect(P) <= B Int Collect(Q)";
 by (blast_tac (claset() addIs [subs RS subsetD, PQimp RS mp]) 1);
diff -r c9ad6bbf3a34 -r 7a8975451a89 src/HOL/subset.ML
--- a/src/HOL/subset.ML	Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/subset.ML	Thu Aug 13 18:14:26 1998 +0200
@@ -12,32 +12,28 @@
 qed_goal "subset_insertI" Set.thy "B <= insert a B"
  (fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]);
 
-goal Set.thy "!!x. x ~: A ==> (A <= insert x B) = (A <= B)";
+Goal "x ~: A ==> (A <= insert x B) = (A <= B)";
 by (Blast_tac 1);
 qed "subset_insert";
 
 (*** Big Union -- least upper bound of a set  ***)
 
-val prems = goal Set.thy
-    "B:A ==> B <= Union(A)";
-by (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1));
+Goal "B:A ==> B <= Union(A)";
+by (REPEAT (ares_tac [subsetI,UnionI] 1));
 qed "Union_upper";
 
-val [prem] = goal Set.thy
-    "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C";
+val [prem] = Goal "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C";
 by (rtac subsetI 1);
 by (REPEAT (eresolve_tac [asm_rl, UnionE, prem RS subsetD] 1));
 qed "Union_least";
 
 (** General union **)
 
-val prems = goal Set.thy
-    "a:A ==> B(a) <= (UN x:A. B(x))";
-by (REPEAT (ares_tac (prems@[UN_I RS subsetI]) 1));
+Goal "a:A ==> B(a) <= (UN x:A. B(x))";
+by (Blast_tac 1);
 qed "UN_upper";
 
-val [prem] = goal Set.thy
-    "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C";
+val [prem] = Goal "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C";
 by (rtac subsetI 1);
 by (REPEAT (eresolve_tac [asm_rl, UN_E, prem RS subsetD] 1));
 qed "UN_least";
@@ -45,52 +41,49 @@
 
 (*** Big Intersection -- greatest lower bound of a set ***)
 
-goal Set.thy "!!B. B:A ==> Inter(A) <= B";
+Goal "B:A ==> Inter(A) <= B";
 by (Blast_tac 1);
 qed "Inter_lower";
 
-val [prem] = goal Set.thy
-    "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)";
+val [prem] = Goal "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)";
 by (rtac (InterI RS subsetI) 1);
 by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
 qed "Inter_greatest";
 
-val prems = goal Set.thy "a:A ==> (INT x:A. B(x)) <= B(a)";
-by (rtac subsetI 1);
-by (REPEAT (resolve_tac prems 1 ORELSE etac INT_D 1));
+Goal "a:A ==> (INT x:A. B(x)) <= B(a)";
+by (Blast_tac 1);
 qed "INT_lower";
 
-val [prem] = goal Set.thy
-    "[| !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))";
+val [prem] = Goal "[| !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))";
 by (rtac (INT_I RS subsetI) 1);
 by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
 qed "INT_greatest";
 
 (*** Finite Union -- the least upper bound of 2 sets ***)
 
-goal Set.thy "A <= A Un B";
+Goal "A <= A Un B";
 by (Blast_tac 1);
 qed "Un_upper1";
 
-goal Set.thy "B <= A Un B";
+Goal "B <= A Un B";
 by (Blast_tac 1);
 qed "Un_upper2";
 
-goal Set.thy "!!C. [| A<=C;  B<=C |] ==> A Un B <= C";
+Goal "[| A<=C;  B<=C |] ==> A Un B <= C";
 by (Blast_tac 1);
 qed "Un_least";
 
 (*** Finite Intersection -- the greatest lower bound of 2 sets *)
 
-goal Set.thy "A Int B <= A";
+Goal "A Int B <= A";
 by (Blast_tac 1);
 qed "Int_lower1";
 
-goal Set.thy "A Int B <= B";
+Goal "A Int B <= B";
 by (Blast_tac 1);
 qed "Int_lower2";
 
-goal Set.thy "!!C. [| C<=A;  C<=B |] ==> C <= A Int B";
+Goal "[| C<=A;  C<=B |] ==> C <= A Int B";
 by (Blast_tac 1);
 qed "Int_greatest";
 
@@ -101,14 +94,14 @@
 
 (*** Monotonicity ***)
 
-val [prem] = goal Set.thy "mono(f) ==> f(A) Un f(B) <= f(A Un B)";
+Goal "mono(f) ==> f(A) Un f(B) <= f(A Un B)";
 by (rtac Un_least 1);
-by (rtac (Un_upper1 RS (prem RS monoD)) 1);
-by (rtac (Un_upper2 RS (prem RS monoD)) 1);
+by (etac (Un_upper1 RSN (2,monoD)) 1);
+by (etac (Un_upper2 RSN (2,monoD)) 1);
 qed "mono_Un";
 
-val [prem] = goal Set.thy "mono(f) ==> f(A Int B) <= f(A) Int f(B)";
+Goal "mono(f) ==> f(A Int B) <= f(A) Int f(B)";
 by (rtac Int_greatest 1);
-by (rtac (Int_lower1 RS (prem RS monoD)) 1);
-by (rtac (Int_lower2 RS (prem RS monoD)) 1);
+by (etac (Int_lower1 RSN (2,monoD)) 1);
+by (etac (Int_lower2 RSN (2,monoD)) 1);
 qed "mono_Int";