# HG changeset patch
# User paulson
# Date 903112648 -7200
# Node ID f8848433d24074e5c5bfc4b2a84c9a6f5b33739a
# Parent  79b326bceafb00a59daa8e47e18d4036e33a908a
got rid of some goal thy commands

diff -r 79b326bceafb -r f8848433d240 src/ZF/AC.ML
--- a/src/ZF/AC.ML	Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/AC.ML	Fri Aug 14 18:37:28 1998 +0200
@@ -61,3 +61,9 @@
 by (REPEAT (ares_tac [non_empty_family] 1));
 qed "AC_Pi0";
 
+(*Used in Zorn.ML*)
+Goal "[| ch : (PROD X:Pow(S) - {0}. X);  X<=S;  X~=S |] ==> ch ` (S-X) : S-X";
+by (etac apply_type 1);
+by (blast_tac (claset() addSEs [equalityE]) 1);
+qed "choice_Diff";
+
diff -r 79b326bceafb -r f8848433d240 src/ZF/Fixedpt.ML
--- a/src/ZF/Fixedpt.ML	Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/Fixedpt.ML	Fri Aug 14 18:37:28 1998 +0200
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-For fixedpt.thy.  Least and greatest fixed points; the Knaster-Tarski Theorem
+Least and greatest fixed points; the Knaster-Tarski Theorem
 
 Proved in the lattice of subsets of D, namely Pow(D), with Inter as glb
 *)
@@ -12,7 +12,7 @@
 
 (*** Monotone operators ***)
 
-val prems = goalw Fixedpt.thy [bnd_mono_def]
+val prems = Goalw [bnd_mono_def]
     "[| h(D)<=D;  \
 \       !!W X. [| W<=D;  X<=D;  W<=X |] ==> h(W) <= h(X)  \
 \    |] ==> bnd_mono(D,h)";  
@@ -20,14 +20,12 @@
      ORELSE etac subset_trans 1));
 qed "bnd_monoI";
 
-val [major] = goalw Fixedpt.thy [bnd_mono_def] "bnd_mono(D,h) ==> h(D) <= D";
-by (rtac (major RS conjunct1) 1);
+Goalw [bnd_mono_def] "bnd_mono(D,h) ==> h(D) <= D";
+by (etac conjunct1 1);
 qed "bnd_monoD1";
 
-val major::prems = goalw Fixedpt.thy [bnd_mono_def]
-    "[| bnd_mono(D,h);  W<=X;  X<=D |] ==> h(W) <= h(X)";
-by (rtac (major RS conjunct2 RS spec RS spec RS mp RS mp) 1);
-by (REPEAT (resolve_tac prems 1));
+Goalw [bnd_mono_def] "[| bnd_mono(D,h);  W<=X;  X<=D |] ==> h(W) <= h(X)";
+by (Blast_tac 1);
 qed "bnd_monoD2";
 
 val [major,minor] = goal Fixedpt.thy
@@ -71,7 +69,7 @@
 by (rtac lfp_subset 1);
 qed "def_lfp_subset";
 
-val prems = goalw Fixedpt.thy [lfp_def]
+val prems = Goalw [lfp_def]
     "[| h(D) <= D;  !!X. [| h(X) <= X;  X<=D |] ==> A<=X |] ==> \
 \    A <= lfp(D,h)";
 by (rtac (Pow_top RS CollectI RS Inter_greatest) 1);
@@ -85,11 +83,10 @@
 by (REPEAT (resolve_tac prems 1));
 qed "lfp_lemma1";
 
-val [hmono] = goal Fixedpt.thy
-    "bnd_mono(D,h) ==> h(lfp(D,h)) <= lfp(D,h)";
+Goal "bnd_mono(D,h) ==> h(lfp(D,h)) <= lfp(D,h)";
 by (rtac (bnd_monoD1 RS lfp_greatest) 1);
 by (rtac lfp_lemma1 2);
-by (REPEAT (ares_tac [hmono] 1));
+by (REPEAT (assume_tac 1));
 qed "lfp_lemma2";
 
 val [hmono] = goal Fixedpt.thy
@@ -101,9 +98,8 @@
 by (REPEAT (rtac lfp_subset 1));
 qed "lfp_lemma3";
 
-val prems = goal Fixedpt.thy
-    "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))";
-by (REPEAT (resolve_tac (prems@[equalityI,lfp_lemma2,lfp_lemma3]) 1));
+Goal "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))";
+by (REPEAT (ares_tac [equalityI,lfp_lemma2,lfp_lemma3] 1));
 qed "lfp_Tarski";
 
 (*Definition form, to control unfolding*)
@@ -115,7 +111,7 @@
 
 (*** General induction rule for least fixedpoints ***)
 
-val [hmono,indstep] = goal Fixedpt.thy
+val [hmono,indstep] = Goal
     "[| bnd_mono(D,h);  !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \
 \    |] ==> h(Collect(lfp(D,h),P)) <= Collect(lfp(D,h),P)";
 by (rtac subsetI 1);
@@ -128,7 +124,7 @@
 
 (*This rule yields an induction hypothesis in which the components of a
   data structure may be assumed to be elements of lfp(D,h)*)
-val prems = goal Fixedpt.thy
+val prems = Goal
     "[| bnd_mono(D,h);  a : lfp(D,h);                   \
 \       !!x. x : h(Collect(lfp(D,h),P)) ==> P(x)        \
 \    |] ==> P(a)";
@@ -138,7 +134,7 @@
 qed "induct";
 
 (*Definition form, to control unfolding*)
-val rew::prems = goal Fixedpt.thy
+val rew::prems = Goal
     "[| A == lfp(D,h);  bnd_mono(D,h);  a:A;   \
 \       !!x. x : h(Collect(A,P)) ==> P(x) \
 \    |] ==> P(a)";
@@ -157,7 +153,7 @@
 
 (*Monotonicity of lfp, where h precedes i under a domain-like partial order
   monotonicity of h is not strictly necessary; h must be bounded by D*)
-val [hmono,imono,subhi] = goal Fixedpt.thy
+val [hmono,imono,subhi] = Goal
     "[| bnd_mono(D,h);  bnd_mono(E,i);          \
 \       !!X. X<=D ==> h(X) <= i(X)  |] ==> lfp(D,h) <= lfp(E,i)";
 by (rtac (bnd_monoD1 RS lfp_greatest) 1);
@@ -170,7 +166,7 @@
 
 (*This (unused) version illustrates that monotonicity is not really needed,
   but both lfp's must be over the SAME set D;  Inter is anti-monotonic!*)
-val [isubD,subhi] = goal Fixedpt.thy
+val [isubD,subhi] = Goal
     "[| i(D) <= D;  !!X. X<=D ==> h(X) <= i(X)  |] ==> lfp(D,h) <= lfp(D,i)";
 by (rtac lfp_greatest 1);
 by (rtac isubD 1);
@@ -183,10 +179,9 @@
 (**** Proof of Knaster-Tarski Theorem for the gfp ****)
 
 (*gfp contains each post-fixedpoint that is contained in D*)
-val prems = goalw Fixedpt.thy [gfp_def]
-    "[| A <= h(A);  A<=D |] ==> A <= gfp(D,h)";
+Goalw [gfp_def] "[| A <= h(A);  A<=D |] ==> A <= gfp(D,h)";
 by (rtac (PowI RS CollectI RS Union_upper) 1);
-by (REPEAT (resolve_tac prems 1));
+by (REPEAT (assume_tac 1));
 qed "gfp_upperbound";
 
 Goalw [gfp_def] "gfp(D,h) <= D";
@@ -199,7 +194,7 @@
 by (rtac gfp_subset 1);
 qed "def_gfp_subset";
 
-val hmono::prems = goalw Fixedpt.thy [gfp_def]
+val hmono::prems = Goalw [gfp_def]
     "[| bnd_mono(D,h);  !!X. [| X <= h(X);  X<=D |] ==> X<=A |] ==> \
 \    gfp(D,h) <= A";
 by (fast_tac (subset_cs addIs ((hmono RS bnd_monoD1)::prems)) 1);
@@ -213,11 +208,10 @@
 by (REPEAT (resolve_tac prems 1));
 qed "gfp_lemma1";
 
-val [hmono] = goal Fixedpt.thy
-    "bnd_mono(D,h) ==> gfp(D,h) <= h(gfp(D,h))";
+Goal "bnd_mono(D,h) ==> gfp(D,h) <= h(gfp(D,h))";
 by (rtac gfp_least 1);
 by (rtac gfp_lemma1 2);
-by (REPEAT (ares_tac [hmono] 1));
+by (REPEAT (assume_tac 1));
 qed "gfp_lemma2";
 
 val [hmono] = goal Fixedpt.thy
@@ -228,9 +222,8 @@
 by (REPEAT (rtac ([hmono, gfp_subset] MRS bnd_mono_subset) 1));
 qed "gfp_lemma3";
 
-val prems = goal Fixedpt.thy
-    "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))";
-by (REPEAT (resolve_tac (prems@[equalityI,gfp_lemma2,gfp_lemma3]) 1));
+Goal "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))";
+by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1));
 qed "gfp_Tarski";
 
 (*Definition form, to control unfolding*)
@@ -275,7 +268,7 @@
 qed "def_coinduct";
 
 (*Lemma used immediately below!*)
-val [subsA,XimpP] = goal ZF.thy
+val [subsA,XimpP] = Goal
     "[| X <= A;  !!z. z:X ==> P(z) |] ==> X <= Collect(A,P)";
 by (rtac (subsA RS subsetD RS CollectI RS subsetI) 1);
 by (assume_tac 1);
@@ -283,7 +276,7 @@
 qed "subset_Collect";
 
 (*The version used in the induction/coinduction package*)
-val prems = goal Fixedpt.thy
+val prems = Goal
     "[| A == gfp(D, %w. Collect(D,P(w)));  bnd_mono(D, %w. Collect(D,P(w)));  \
 \       a: X;  X <= D;  !!z. z: X ==> P(X Un A, z) |] ==> \
 \    a : A";
@@ -292,7 +285,7 @@
 qed "def_Collect_coinduct";
 
 (*Monotonicity of gfp!*)
-val [hmono,subde,subhi] = goal Fixedpt.thy
+val [hmono,subde,subhi] = Goal
     "[| bnd_mono(D,h);  D <= E;                 \
 \       !!X. X<=D ==> h(X) <= i(X)  |] ==> gfp(D,h) <= gfp(E,i)";
 by (rtac gfp_upperbound 1);
diff -r 79b326bceafb -r f8848433d240 src/ZF/List.ML
--- a/src/ZF/List.ML	Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/List.ML	Fri Aug 14 18:37:28 1998 +0200
@@ -55,7 +55,7 @@
 by (REPEAT (ares_tac [list_subset_univ RS subsetD] 1));
 qed "list_into_univ";
 
-val major::prems = goal List.thy
+val major::prems = Goal
     "[| l: list(A);    \
 \       c: C(Nil);       \
 \       !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(Cons(x,y))  \
@@ -142,7 +142,7 @@
 
 
 (*Type checking -- proved by induction, as usual*)
-val prems = goal List.thy
+val prems = Goal
     "[| l: list(A);    \
 \       c: C(Nil);       \
 \       !!x y r. [| x:A;  y: list(A);  r: C(y) |] ==> h(x,y,r): C(Cons(x,y))  \
@@ -153,14 +153,12 @@
 
 (** Versions for use with definitions **)
 
-val [rew] = goal List.thy
-    "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c";
+val [rew] = Goal "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c";
 by (rewtac rew);
 by (rtac list_rec_Nil 1);
 qed "def_list_rec_Nil";
 
-val [rew] = goal List.thy
-    "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))";
+val [rew] = Goal "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))";
 by (rewtac rew);
 by (rtac list_rec_Cons 1);
 qed "def_list_rec_Cons";
@@ -173,13 +171,13 @@
 val [map_Nil,map_Cons] = list_recs map_def;
 Addsimps [map_Nil, map_Cons];
 
-val prems = goalw List.thy [map_def] 
+val prems = Goalw [map_def] 
     "[| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)";
 by (REPEAT (ares_tac (prems @ list.intrs @ [list_rec_type]) 1));
 qed "map_type";
 
-val [major] = goal List.thy "l: list(A) ==> map(h,l) : list({h(u). u:A})";
-by (rtac (major RS map_type) 1);
+Goal "l: list(A) ==> map(h,l) : list({h(u). u:A})";
+by (etac map_type 1);
 by (etac RepFunI 1);
 qed "map_type2";
 
@@ -263,35 +261,30 @@
 
 (*** theorems about map ***)
 
-val prems = goal List.thy
-    "l: list(A) ==> map(%u. u, l) = l";
-by (list_ind_tac "l" prems 1);
+Goal "l: list(A) ==> map(%u. u, l) = l";
+by (list_ind_tac "l" [] 1);
 by (ALLGOALS Asm_simp_tac);
 qed "map_ident";
 
-val prems = goal List.thy
-    "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)";
-by (list_ind_tac "l" prems 1);
+Goal "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)";
+by (list_ind_tac "l" [] 1);
 by (ALLGOALS Asm_simp_tac);
 qed "map_compose";
 
-val prems = goal List.thy
-    "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
-by (list_ind_tac "xs" prems 1);
+Goal "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
+by (list_ind_tac "xs" [] 1);
 by (ALLGOALS Asm_simp_tac);
 qed "map_app_distrib";
 
-val prems = goal List.thy
-    "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
-by (list_ind_tac "ls" prems 1);
+Goal "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
+by (list_ind_tac "ls" [] 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
 qed "map_flat";
 
-val prems = goal List.thy
-    "l: list(A) ==> \
+Goal "l: list(A) ==> \
 \    list_rec(map(h,l), c, d) = \
 \    list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
-by (list_ind_tac "l" prems 1);
+by (list_ind_tac "l" [] 1);
 by (ALLGOALS Asm_simp_tac);
 qed "list_rec_map";
 
@@ -300,23 +293,20 @@
 (* c : list(Collect(B,P)) ==> c : list(B) *)
 bind_thm ("list_CollectD", (Collect_subset RS list_mono RS subsetD));
 
-val prems = goal List.thy
-    "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
-by (list_ind_tac "l" prems 1);
+Goal "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
+by (list_ind_tac "l" [] 1);
 by (ALLGOALS Asm_simp_tac);
 qed "map_list_Collect";
 
 (*** theorems about length ***)
 
-val prems = goal List.thy
-    "xs: list(A) ==> length(map(h,xs)) = length(xs)";
-by (list_ind_tac "xs" prems 1);
+Goal "xs: list(A) ==> length(map(h,xs)) = length(xs)";
+by (list_ind_tac "xs" [] 1);
 by (ALLGOALS Asm_simp_tac);
 qed "length_map";
 
-val prems = goal List.thy
-    "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
-by (list_ind_tac "xs" prems 1);
+Goal "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
+by (list_ind_tac "xs" [] 1);
 by (ALLGOALS Asm_simp_tac);
 qed "length_app";
 
@@ -324,15 +314,13 @@
    Used for rewriting below*)
 val add_commute_succ = nat_succI RSN (2,add_commute);
 
-val prems = goal List.thy
-    "xs: list(A) ==> length(rev(xs)) = length(xs)";
-by (list_ind_tac "xs" prems 1);
+Goal "xs: list(A) ==> length(rev(xs)) = length(xs)";
+by (list_ind_tac "xs" [] 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app, add_commute_succ])));
 qed "length_rev";
 
-val prems = goal List.thy
-    "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
-by (list_ind_tac "ls" prems 1);
+Goal "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
+by (list_ind_tac "ls" [] 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app])));
 qed "length_flat";
 
@@ -364,26 +352,25 @@
 
 (*** theorems about app ***)
 
-val [major] = goal List.thy "xs: list(A) ==> xs@Nil=xs";
-by (rtac (major RS list.induct) 1);
+Goal "xs: list(A) ==> xs@Nil=xs";
+by (etac list.induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "app_right_Nil";
 
-val prems = goal List.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
-by (list_ind_tac "xs" prems 1);
+Goal "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
+by (list_ind_tac "xs" [] 1);
 by (ALLGOALS Asm_simp_tac);
 qed "app_assoc";
 
-val prems = goal List.thy
-    "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
-by (list_ind_tac "ls" prems 1);
+Goal "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
+by (list_ind_tac "ls" [] 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc])));
 qed "flat_app_distrib";
 
 (*** theorems about rev ***)
 
-val prems = goal List.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
-by (list_ind_tac "l" prems 1);
+Goal "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
+by (list_ind_tac "l" [] 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
 qed "rev_map_distrib";
 
@@ -396,14 +383,13 @@
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_right_Nil,app_assoc])));
 qed "rev_app_distrib";
 
-val prems = goal List.thy "l: list(A) ==> rev(rev(l))=l";
-by (list_ind_tac "l" prems 1);
+Goal "l: list(A) ==> rev(rev(l))=l";
+by (list_ind_tac "l" [] 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [rev_app_distrib])));
 qed "rev_rev_ident";
 
-val prems = goal List.thy
-    "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
-by (list_ind_tac "ls" prems 1);
+Goal "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
+by (list_ind_tac "ls" [] 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps 
        [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
 qed "rev_flat";
@@ -411,34 +397,30 @@
 
 (*** theorems about list_add ***)
 
-val prems = goal List.thy
-    "[| xs: list(nat);  ys: list(nat) |] ==> \
+Goal "[| xs: list(nat);  ys: list(nat) |] ==> \
 \    list_add(xs@ys) = list_add(ys) #+ list_add(xs)";
-by (cut_facts_tac prems 1);
-by (list_ind_tac "xs" prems 1);
+by (list_ind_tac "xs" [] 1);
 by (ALLGOALS 
     (asm_simp_tac (simpset() addsimps [add_0_right, add_assoc RS sym])));
 by (rtac (add_commute RS subst_context) 1);
 by (REPEAT (ares_tac [refl, list_add_type] 1));
 qed "list_add_app";
 
-val prems = goal List.thy
-    "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
-by (list_ind_tac "l" prems 1);
+Goal "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
+by (list_ind_tac "l" [] 1);
 by (ALLGOALS
     (asm_simp_tac (simpset() addsimps [list_add_app, add_0_right])));
 qed "list_add_rev";
 
-val prems = goal List.thy
-    "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
-by (list_ind_tac "ls" prems 1);
+Goal "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
+by (list_ind_tac "ls" [] 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app])));
 by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1));
 qed "list_add_flat";
 
 (** New induction rule **)
 
-val major::prems = goal List.thy
+val major::prems = Goal
     "[| l: list(A);  \
 \       P(Nil);        \
 \       !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(y @ [x]) \
diff -r 79b326bceafb -r f8848433d240 src/ZF/Ordinal.ML
--- a/src/ZF/Ordinal.ML	Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/Ordinal.ML	Fri Aug 14 18:37:28 1998 +0200
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-For Ordinal.thy.  Ordinals in Zermelo-Fraenkel Set Theory 
+Ordinals in Zermelo-Fraenkel Set Theory 
 *)
 
 open Ordinal;
@@ -73,12 +73,12 @@
 by (Blast_tac 1);
 qed "Transset_Union";
 
-val [Transprem] = goalw Ordinal.thy [Transset_def]
+val [Transprem] = Goalw [Transset_def]
     "[| !!i. i:A ==> Transset(i) |] ==> Transset(Union(A))";
 by (blast_tac (claset() addDs [Transprem RS bspec RS subsetD]) 1);
 qed "Transset_Union_family";
 
-val [prem,Transprem] = goalw Ordinal.thy [Transset_def]
+val [prem,Transprem] = Goalw [Transset_def]
     "[| j:A;  !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))";
 by (cut_facts_tac [prem] 1);
 by (blast_tac (claset() addDs [Transprem RS bspec RS subsetD]) 1);
@@ -86,19 +86,18 @@
 
 (*** Natural Deduction rules for Ord ***)
 
-val prems = goalw Ordinal.thy [Ord_def]
+val prems = Goalw [Ord_def]
     "[| Transset(i);  !!x. x:i ==> Transset(x) |]  ==>  Ord(i)";
 by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
 qed "OrdI";
 
-val [major] = goalw Ordinal.thy [Ord_def]
-    "Ord(i) ==> Transset(i)";
-by (rtac (major RS conjunct1) 1);
+Goalw [Ord_def] "Ord(i) ==> Transset(i)";
+by (Blast_tac 1);
 qed "Ord_is_Transset";
 
-val [major,minor] = goalw Ordinal.thy [Ord_def]
+Goalw [Ord_def]
     "[| Ord(i);  j:i |] ==> Transset(j) ";
-by (rtac (minor RS (major RS conjunct2 RS bspec)) 1);
+by (Blast_tac 1);
 qed "Ord_contains_Transset";
 
 (*** Lemmas for ordinals ***)
@@ -159,7 +158,7 @@
 by (blast_tac (claset() addSIs [Transset_Int]) 1);
 qed "Ord_Int";
 
-val nonempty::prems = goal Ordinal.thy
+val nonempty::prems = Goal
     "[| j:A;  !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))";
 by (rtac (nonempty RS Transset_Inter_family RS OrdI) 1);
 by (rtac Ord_is_Transset 1);
@@ -167,7 +166,7 @@
      ORELSE etac InterD 1));
 qed "Ord_Inter";
 
-val jmemA::prems = goal Ordinal.thy
+val jmemA::prems = Goal
     "[| j:A;  !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))";
 by (rtac (jmemA RS RepFunI RS Ord_Inter) 1);
 by (etac RepFunE 1);
@@ -194,7 +193,7 @@
 by (REPEAT (ares_tac [conjI] 1));
 qed "ltI";
 
-val major::prems = goalw Ordinal.thy [lt_def]
+val major::prems = Goalw [lt_def]
     "[| i<j;  [| i:j;  Ord(i);  Ord(j) |] ==> P |] ==> P";
 by (rtac (major RS conjE) 1);
 by (REPEAT (ares_tac (prems@[Ord_in_Ord]) 1));
@@ -258,12 +257,12 @@
 
 val le_refl = refl RS le_eqI;
 
-val [prem] = goal Ordinal.thy "(~ (i=j & Ord(j)) ==> i<j) ==> i le j";
+val [prem] = Goal "(~ (i=j & Ord(j)) ==> i<j) ==> i le j";
 by (rtac (disjCI RS (le_iff RS iffD2)) 1);
 by (etac prem 1);
 qed "leCI";
 
-val major::prems = goal Ordinal.thy
+val major::prems = Goal
     "[| i le j;  i<j ==> P;  [| i=j;  Ord(j) |] ==> P |] ==> P";
 by (rtac (major RS (le_iff RS iffD1 RS disjE)) 1);
 by (DEPTH_SOLVE (ares_tac prems 1 ORELSE etac conjE 1));
@@ -298,7 +297,7 @@
 by (REPEAT (ares_tac [conjI, Memrel_iff RS iffD2] 1));
 qed "MemrelI";
 
-val [major,minor] = goal Ordinal.thy
+val [major,minor] = Goal
     "[| <a,b> : Memrel(A);  \
 \       [| a: A;  b: A;  a:b |]  ==> P \
 \    |]  ==> P";
@@ -357,7 +356,7 @@
 (*** Transfinite induction ***)
 
 (*Epsilon induction over a transitive set*)
-val major::prems = goalw Ordinal.thy [Transset_def]
+val major::prems = Goalw [Transset_def]
     "[| i: k;  Transset(k);                          \
 \       !!x.[| x: k;  ALL y:x. P(y) |] ==> P(x) \
 \    |]  ==>  P(i)";
@@ -373,7 +372,7 @@
 val Ord_induct = Ord_is_Transset RSN (2, Transset_induct);
 
 (*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
-val [major,indhyp] = goal Ordinal.thy
+val [major,indhyp] = Goal
     "[| Ord(i); \
 \       !!x.[| Ord(x);  ALL y:x. P(y) |] ==> P(x) \
 \    |]  ==>  P(i)";
@@ -397,29 +396,28 @@
 
 (** Proving that < is a linear ordering on the ordinals **)
 
-val prems = goal Ordinal.thy
-    "Ord(i) ==> (ALL j. Ord(j) --> i:j | i=j | j:i)";
-by (trans_ind_tac "i" prems 1);
+Goal "Ord(i) ==> (ALL j. Ord(j) --> i:j | i=j | j:i)";
+by (etac trans_induct 1);
 by (rtac (impI RS allI) 1);
 by (trans_ind_tac "j" [] 1);
 by (DEPTH_SOLVE (Step_tac 1 ORELSE Ord_trans_tac 1));
 qed_spec_mp "Ord_linear";
 
 (*The trichotomy law for ordinals!*)
-val ordi::ordj::prems = goalw Ordinal.thy [lt_def]
+val ordi::ordj::prems = Goalw [lt_def]
     "[| Ord(i);  Ord(j);  i<j ==> P;  i=j ==> P;  j<i ==> P |] ==> P";
 by (rtac ([ordi,ordj] MRS Ord_linear RS disjE) 1);
 by (etac disjE 2);
 by (DEPTH_SOLVE (ares_tac ([ordi,ordj,conjI] @ prems) 1));
 qed "Ord_linear_lt";
 
-val prems = goal Ordinal.thy
+val prems = Goal
     "[| Ord(i);  Ord(j);  i<j ==> P;  j le i ==> P |]  ==> P";
 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
 by (DEPTH_SOLVE (ares_tac ([leI, sym RS le_eqI] @ prems) 1));
 qed "Ord_linear2";
 
-val prems = goal Ordinal.thy
+val prems = Goal
     "[| Ord(i);  Ord(j);  i le j ==> P;  j le i ==> P |]  ==> P";
 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
 by (DEPTH_SOLVE (ares_tac ([leI,le_eqI] @ prems) 1));
@@ -489,7 +487,7 @@
 qed "le_succ_iff";
 
 (*Just a variant of subset_imp_le*)
-val [ordi,ordj,minor] = goal Ordinal.thy
+val [ordi,ordj,minor] = Goal
     "[| Ord(i);  Ord(j);  !!x. x<j ==> x<i |] ==> j le i";
 by (REPEAT_FIRST (ares_tac [notI RS not_lt_imp_le, ordi, ordj]));
 by (etac (minor RS lt_irrefl) 1);
@@ -581,12 +579,12 @@
 
 (*** Results about limits ***)
 
-val prems = goal Ordinal.thy "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))";
+val prems = Goal "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))";
 by (rtac (Ord_is_Transset RS Transset_Union_family RS OrdI) 1);
 by (REPEAT (etac UnionE 1 ORELSE ares_tac ([Ord_contains_Transset]@prems) 1));
 qed "Ord_Union";
 
-val prems = goal Ordinal.thy
+val prems = Goal
     "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))";
 by (rtac Ord_Union 1);
 by (etac RepFunE 1);
@@ -595,27 +593,27 @@
 qed "Ord_UN";
 
 (* No < version; consider (UN i:nat.i)=nat *)
-val [ordi,limit] = goal Ordinal.thy
+val [ordi,limit] = Goal
     "[| Ord(i);  !!x. x:A ==> b(x) le i |] ==> (UN x:A. b(x)) le i";
 by (rtac (le_imp_subset RS UN_least RS subset_imp_le) 1);
 by (REPEAT (ares_tac [ordi, Ord_UN, limit] 1 ORELSE etac (limit RS ltE) 1));
 qed "UN_least_le";
 
-val [jlti,limit] = goal Ordinal.thy
+val [jlti,limit] = Goal
     "[| j<i;  !!x. x:A ==> b(x)<j |] ==> (UN x:A. succ(b(x))) < i";
 by (rtac (jlti RS ltE) 1);
 by (rtac (UN_least_le RS lt_trans2) 1);
 by (REPEAT (ares_tac [jlti, succ_leI, limit] 1));
 qed "UN_succ_least_lt";
 
-val prems = goal Ordinal.thy
+val prems = Goal
     "[| a: A;  i le b(a);  !!x. x:A ==> Ord(b(x)) |] ==> i le (UN x:A. b(x))";
 by (resolve_tac (prems RL [ltE]) 1);
 by (rtac (le_imp_subset RS subset_trans RS subset_imp_le) 1);
 by (REPEAT (ares_tac (prems @ [UN_upper, Ord_UN]) 1));
 qed "UN_upper_le";
 
-val [leprem] = goal Ordinal.thy
+val [leprem] = Goal
     "[| !!x. x:A ==> c(x) le d(x) |] ==> (UN x:A. c(x)) le (UN x:A. d(x))";
 by (rtac UN_least_le 1);
 by (rtac UN_upper_le 2);
@@ -679,7 +677,7 @@
                       addSDs [Ord_succD]) 1);
 qed "Ord_cases_disj";
 
-val major::prems = goal Ordinal.thy
+val major::prems = Goal
     "[| Ord(i);                 \
 \       i=0                          ==> P;     \
 \       !!j. [| Ord(j); i=succ(j) |] ==> P;     \
@@ -689,7 +687,7 @@
 by (REPEAT (eresolve_tac (prems@[asm_rl, disjE, exE, conjE]) 1));
 qed "Ord_cases";
 
-val major::prems = goal Ordinal.thy
+val major::prems = Goal
      "[| Ord(i);                \
 \        P(0);                  \
 \        !!x. [| Ord(x);  P(x) |] ==> P(succ(x));       \
diff -r 79b326bceafb -r f8848433d240 src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/Perm.ML	Fri Aug 14 18:37:28 1998 +0200
@@ -33,7 +33,7 @@
 by (blast_tac (claset() addIs prems) 1);
 qed "f_imp_surjective";
 
-val prems = goal Perm.thy
+val prems = Goal
     "[| !!x. x:A ==> c(x): B;           \
 \       !!y. y:B ==> d(y): A;           \
 \       !!y. y:B ==> c(d(y)) = y        \
@@ -74,7 +74,7 @@
 by (deepen_tac (claset() addEs [subst_context RS box_equals]) 0 1);
 bind_thm ("f_imp_injective", ballI RSN (2,result()));
 
-val prems = goal Perm.thy
+val prems = Goal
     "[| !!x. x:A ==> c(x): B;           \
 \       !!x. x:A ==> d(c(x)) = x        \
 \    |] ==> (lam x:A. c(x)) : inj(A,B)";
@@ -185,10 +185,9 @@
 
 val left_inverse_bij = bij_is_inj RS left_inverse;
 
-val prems = goal Perm.thy
-    "[| f: A->B;  converse(f): C->A;  b: C |] ==> f`(converse(f)`b) = b";
+Goal "[| f: A->B;  converse(f): C->A;  b: C |] ==> f`(converse(f)`b) = b";
 by (rtac (apply_Pair RS (converseD RS apply_equality)) 1);
-by (REPEAT (resolve_tac prems 1));
+by (REPEAT (assume_tac 1));
 qed "right_inverse_lemma";
 
 (*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse?
@@ -337,7 +336,7 @@
 Addsimps [comp_fun_apply];
 
 (*Simplifies compositions of lambda-abstractions*)
-val [prem] = goal Perm.thy
+val [prem] = Goal
     "[| !!x. x:A ==> b(x): B    \
 \    |] ==> (lam y:B. c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))";
 by (rtac fun_extension 1);
@@ -513,11 +512,10 @@
                           box_equals, restrict] 1));
 qed "restrict_inj";
 
-val prems = goal Perm.thy 
-    "[| f: Pi(A,B);  C<=A |] ==> restrict(f,C): surj(C, f``C)";
+Goal "[| f: Pi(A,B);  C<=A |] ==> restrict(f,C): surj(C, f``C)";
 by (rtac (restrict_image RS subst) 1);
 by (rtac (restrict_type2 RS surj_image) 3);
-by (REPEAT (resolve_tac prems 1));
+by (REPEAT (assume_tac 1));
 qed "restrict_surj";
 
 Goalw [inj_def,bij_def]
diff -r 79b326bceafb -r f8848433d240 src/ZF/QUniv.ML
--- a/src/ZF/QUniv.ML	Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/QUniv.ML	Fri Aug 14 18:37:28 1998 +0200
@@ -160,42 +160,6 @@
 bind_thm ("bool_into_quniv", bool_subset_quniv RS subsetD);
 
 
-(**** Properties of Vfrom analogous to the "take-lemma" ****)
-
-(*** Intersecting a*b with Vfrom... ***)
-
-(*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*)
-goal Univ.thy
-    "!!X. [| {a,b} : Vfrom(X,succ(i));  Transset(X) |] ==> \
-\         a: Vfrom(X,i)  &  b: Vfrom(X,i)";
-by (dtac (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1);
-by (assume_tac 1);
-by (Fast_tac 1);
-qed "doubleton_in_Vfrom_D";
-
-(*This weaker version says a, b exist at the same level*)
-bind_thm ("Vfrom_doubleton_D", Transset_Vfrom RS Transset_doubleton_D);
-
-(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
-      implies a, b : Vfrom(X,i), which is useless for induction.
-    Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))
-      implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.
-    The combination gives a reduction by precisely one level, which is
-      most convenient for proofs.
-**)
-
-goalw Univ.thy [Pair_def]
-    "!!X. [| <a,b> : Vfrom(X,succ(i));  Transset(X) |] ==> \
-\         a: Vfrom(X,i)  &  b: Vfrom(X,i)";
-by (blast_tac (claset() addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1);
-qed "Pair_in_Vfrom_D";
-
-goal Univ.thy
- "!!X. Transset(X) ==>          \
-\      (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))";
-by (blast_tac (claset() addSDs [Pair_in_Vfrom_D]) 1);
-qed "product_Int_Vfrom_subset";
-
 (*** Intersecting <a;b> with Vfrom... ***)
 
 Goalw [QPair_def,sum_def]
diff -r 79b326bceafb -r f8848433d240 src/ZF/Rel.ML
--- a/src/ZF/Rel.ML	Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/Rel.ML	Fri Aug 14 18:37:28 1998 +0200
@@ -12,19 +12,18 @@
 
 (* irreflexivity *)
 
-val prems = goalw Rel.thy [irrefl_def]
+val prems = Goalw [irrefl_def]
     "[| !!x. x:A ==> <x,x> ~: r |] ==> irrefl(A,r)";
 by (REPEAT (ares_tac (prems @ [ballI]) 1));
 qed "irreflI";
 
-val prems = goalw Rel.thy [irrefl_def]
-    "[| irrefl(A,r);  x:A |] ==>  <x,x> ~: r";
-by (rtac (prems MRS bspec) 1);
+Goalw [irrefl_def] "[| irrefl(A,r);  x:A |] ==>  <x,x> ~: r";
+by (Blast_tac 1);
 qed "irreflE";
 
 (* symmetry *)
 
-val prems = goalw Rel.thy [sym_def]
+val prems = Goalw [sym_def]
      "[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)";
 by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
 qed "symI";
@@ -35,21 +34,19 @@
 
 (* antisymmetry *)
 
-val prems = goalw Rel.thy [antisym_def]
+val prems = Goalw [antisym_def]
      "[| !!x y.[| <x,y>: r;  <y,x>: r |] ==> x=y |] ==> \
 \     antisym(r)";
 by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
 qed "antisymI";
 
-val prems = goalw Rel.thy [antisym_def]
-     "!!r. [| antisym(r); <x,y>: r;  <y,x>: r |]  ==>  x=y";
+Goalw [antisym_def] "[| antisym(r); <x,y>: r;  <y,x>: r |]  ==>  x=y";
 by (Blast_tac 1);
 qed "antisymE";
 
 (* transitivity *)
 
-Goalw [trans_def]
-    "[| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r";
+Goalw [trans_def] "[| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r";
 by (Blast_tac 1);
 qed "transD";
 
diff -r 79b326bceafb -r f8848433d240 src/ZF/Sum.ML
--- a/src/ZF/Sum.ML	Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/Sum.ML	Fri Aug 14 18:37:28 1998 +0200
@@ -22,7 +22,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 CollectE) 1);
@@ -58,7 +58,7 @@
 
 (** Elimination rules **)
 
-val major::prems = goalw Sum.thy sum_defs
+val major::prems = Goalw sum_defs
     "[| u: A+B;  \
 \       !!x. [| x:A;  u=Inl(x) |] ==> P; \
 \       !!y. [| y:B;  u=Inr(y) |] ==> P \
@@ -141,7 +141,7 @@
 
 Addsimps [case_Inl, case_Inr];
 
-val major::prems = goal Sum.thy
+val major::prems = Goal
     "[| u: A+B; \
 \       !!x. x: A ==> c(x): C(Inl(x));   \
 \       !!y. y: B ==> d(y): C(Inr(y)) \
@@ -158,7 +158,7 @@
 by Auto_tac;
 qed "expand_case";
 
-val major::prems = goal Sum.thy
+val major::prems = Goal
   "[| z: A+B;   \
 \     !!x. x:A ==> c(x)=c'(x);  \
 \     !!y. y:B ==> d(y)=d'(y)   \
diff -r 79b326bceafb -r f8848433d240 src/ZF/Trancl.ML
--- a/src/ZF/Trancl.ML	Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/Trancl.ML	Fri Aug 14 18:37:28 1998 +0200
@@ -14,9 +14,9 @@
 by (Blast_tac 1);
 qed "rtrancl_bnd_mono";
 
-val [prem] = goalw Trancl.thy [rtrancl_def] "r<=s ==> r^* <= s^*";
+Goalw [rtrancl_def] "r<=s ==> r^* <= s^*";
 by (rtac lfp_mono 1);
-by (REPEAT (resolve_tac [rtrancl_bnd_mono, prem, subset_refl, id_mono,
+by (REPEAT (ares_tac [rtrancl_bnd_mono, subset_refl, id_mono,
                          comp_mono, Un_mono, field_mono, Sigma_mono] 1));
 qed "rtrancl_mono";
 
@@ -28,29 +28,27 @@
 bind_thm ("rtrancl_type", (rtrancl_def RS def_lfp_subset));
 
 (*Reflexivity of rtrancl*)
-val [prem] = goal Trancl.thy "[| a: field(r) |] ==> <a,a> : r^*";
+Goal "[| a: field(r) |] ==> <a,a> : r^*";
 by (resolve_tac [rtrancl_unfold RS ssubst] 1);
-by (rtac (prem RS idI RS UnI1) 1);
+by (etac (idI RS UnI1) 1);
 qed "rtrancl_refl";
 
 (*Closure under composition with r  *)
-val prems = goal Trancl.thy
-    "[| <a,b> : r^*;  <b,c> : r |] ==> <a,c> : r^*";
+Goal "[| <a,b> : r^*;  <b,c> : r |] ==> <a,c> : r^*";
 by (resolve_tac [rtrancl_unfold RS ssubst] 1);
 by (rtac (compI RS UnI2) 1);
-by (resolve_tac prems 1);
-by (resolve_tac prems 1);
+by (assume_tac 1);
+by (assume_tac 1);
 qed "rtrancl_into_rtrancl";
 
 (*rtrancl of r contains all pairs in r  *)
-val prems = goal Trancl.thy "<a,b> : r ==> <a,b> : r^*";
+Goal "<a,b> : r ==> <a,b> : r^*";
 by (resolve_tac [rtrancl_refl RS rtrancl_into_rtrancl] 1);
-by (REPEAT (resolve_tac (prems@[fieldI1]) 1));
+by (REPEAT (ares_tac [fieldI1] 1));
 qed "r_into_rtrancl";
 
 (*The premise ensures that r consists entirely of pairs*)
-val prems = goal Trancl.thy "r <= Sigma(A,B) ==> r <= r^*";
-by (cut_facts_tac prems 1);
+Goal "r <= Sigma(A,B) ==> r <= r^*";
 by (blast_tac (claset() addIs [r_into_rtrancl]) 1);
 qed "r_subset_rtrancl";
 
@@ -62,7 +60,7 @@
 
 (** standard induction rule **)
 
-val major::prems = goal Trancl.thy
+val major::prems = Goal
   "[| <a,b> : r^*; \
 \     !!x. x: field(r) ==> P(<x,x>); \
 \     !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |]  ==>  P(<x,z>) |] \
@@ -74,7 +72,7 @@
 (*nice induction rule.
   Tried adding the typing hypotheses y,z:field(r), but these
   caused expensive case splits!*)
-val major::prems = goal Trancl.thy
+val major::prems = Goal
   "[| <a,b> : r^*;                                              \
 \     P(a);                                                     \
 \     !!y z.[| <a,y> : r^*;  <y,z> : r;  P(y) |] ==> P(z)       \
@@ -96,7 +94,7 @@
 qed "trans_rtrancl";
 
 (*elimination of rtrancl -- by induction on a special formula*)
-val major::prems = goal Trancl.thy
+val major::prems = Goal
     "[| <a,b> : r^*;  (a=b) ==> P;                       \
 \       !!y.[| <a,y> : r^*;   <y,b> : r |] ==> P |]      \
 \    ==> P";
@@ -147,7 +145,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)       \
@@ -162,7 +160,7 @@
 qed "trancl_induct";
 
 (*elimination of r^+ -- NOT an induction rule*)
-val major::prems = goal Trancl.thy
+val major::prems = Goal
     "[| <a,b> : r^+;  \
 \       <a,b> : r ==> P; \
 \       !!y.[| <a,y> : r^+; <y,b> : r |] ==> P  \
@@ -178,7 +176,7 @@
 by (blast_tac (claset() addEs [rtrancl_type RS subsetD RS SigmaE2]) 1);
 qed "trancl_type";
 
-val [prem] = goalw Trancl.thy [trancl_def] "r<=s ==> r^+ <= s^+";
-by (REPEAT (resolve_tac [prem, comp_mono, rtrancl_mono] 1));
+Goalw [trancl_def] "r<=s ==> r^+ <= s^+";
+by (REPEAT (ares_tac [comp_mono, rtrancl_mono] 1));
 qed "trancl_mono";
 
diff -r 79b326bceafb -r f8848433d240 src/ZF/Univ.ML
--- a/src/ZF/Univ.ML	Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/Univ.ML	Fri Aug 14 18:37:28 1998 +0200
@@ -107,11 +107,10 @@
 by (REPEAT (ares_tac [doubleton_in_Vfrom] 1));
 qed "Pair_in_Vfrom";
 
-val [prem] = goal Univ.thy
-    "a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))";
+Goal "a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))";
 by (REPEAT (resolve_tac [subset_mem_Vfrom, succ_subsetI] 1));
 by (rtac (Vfrom_mono RSN (2,subset_trans)) 2);
-by (REPEAT (resolve_tac [prem, subset_refl, subset_succI] 1));
+by (REPEAT (ares_tac [subset_refl, subset_succI] 1));
 qed "succ_in_Vfrom";
 
 (*** 0, successor and limit equations fof Vfrom ***)
@@ -140,12 +139,32 @@
 
 (*The premise distinguishes this from Vfrom(A,0);  allowing X=0 forces
   the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *)
+Goal "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
+by (stac Vfrom 1);
+by (rtac equalityI 1);
+(*first inclusion*)
+by (rtac Un_least 1);
+by (rtac (A_subset_Vfrom RS subset_trans) 1);
+by (rtac UN_upper 1);
+by (assume_tac 1);
+by (rtac UN_least 1);
+by (etac UnionE 1);
+by (rtac subset_trans 1);
+by (etac UN_upper 2 THEN stac Vfrom 1 THEN 
+    etac ([UN_upper, Un_upper2] MRS subset_trans) 1);
+(*opposite inclusion*)
+by (rtac UN_least 1);
+by (stac Vfrom 1);
+by (Blast_tac 1);
+qed "Vfrom_Union";
+
 val [prem] = goal Univ.thy "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
 by (stac Vfrom 1);
 by (rtac equalityI 1);
 (*first inclusion*)
 by (rtac Un_least 1);
 by (rtac (A_subset_Vfrom RS subset_trans) 1);
+
 by (rtac (prem RS UN_upper) 1);
 by (rtac UN_least 1);
 by (etac UnionE 1);
@@ -175,7 +194,7 @@
 by (REPEAT (ares_tac [ltD RS UN_I] 1));
 qed "Limit_VfromI";
 
-val prems = goal Univ.thy
+val prems = Goal
     "[| a: Vfrom(A,i);  Limit(i);               \
 \       !!x. [| x<i;  a: Vfrom(A,x) |] ==> R    \
 \    |] ==> R";
@@ -278,8 +297,7 @@
 by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1);
 qed "Transset_Vfrom_succ";
 
-goalw Ordinal.thy [Pair_def,Transset_def]
-    "!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
+Goalw [Pair_def,Transset_def] "[| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
 by (Blast_tac 1);
 qed "Transset_Pair_subset";
 
@@ -297,7 +315,7 @@
 ***)
 
 (*General theorem for membership in Vfrom(A,i) when i is a limit ordinal*)
-val [aprem,bprem,limiti,step] = goal Univ.thy
+val [aprem,bprem,limiti,step] = Goal
   "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);                 \
 \     !!x y j. [| j<i; 1:j; x: Vfrom(A,j); y: Vfrom(A,j) \
 \              |] ==> EX k. h(x,y): Vfrom(A,k) & k<i |] ==>     \
@@ -377,8 +395,7 @@
 qed "fun_in_VLimit";
 
 Goalw [Pi_def]
-    "[| a: Vfrom(A,j);  Transset(A) |] ==> \
-\         Pow(a) : Vfrom(A, succ(succ(j)))";
+    "[| a: Vfrom(A,j);  Transset(A) |] ==> Pow(a) : Vfrom(A, succ(succ(j)))";
 by (dtac Transset_Vfrom 1);
 by (rtac subset_mem_Vfrom 1);
 by (rewtac Transset_def);
@@ -406,8 +423,8 @@
 
 (** Characterisation of the elements of Vset(i) **)
 
-val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i";
-by (rtac (ordi RS trans_induct) 1);
+Goal "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i";
+by (etac trans_induct 1);
 by (stac Vset 1);
 by Safe_tac;
 by (stac rank 1);
@@ -416,8 +433,8 @@
 by (REPEAT (ares_tac [ltI] 1));
 qed_spec_mp "VsetD";
 
-val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
-by (rtac (ordi RS trans_induct) 1);
+Goal "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
+by (etac trans_induct 1);
 by (rtac allI 1);
 by (stac Vset 1);
 by (blast_tac (claset() addSIs [rank_lt RS ltD]) 1);
@@ -458,7 +475,7 @@
 by (etac (rank_lt RS VsetI) 1);
 qed "arg_subset_Vset_rank";
 
-val [iprem] = goal Univ.thy
+val [iprem] = Goal
     "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b";
 by (rtac ([subset_refl, arg_subset_Vset_rank] MRS 
           Int_greatest RS subset_trans) 1);
@@ -490,7 +507,7 @@
 qed "Vrec";
 
 (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
-val rew::prems = goal Univ.thy
+val rew::prems = Goal
     "[| !!x. h(x)==Vrec(x,H) |] ==> \
 \    h(a) = H(a, lam x: Vset(rank(a)). h(x))";
 by (rewtac rew);
@@ -520,7 +537,7 @@
 by (etac (univ_eq_UN RS subst) 1);
 qed "subset_univ_eq_Int";
 
-val [aprem, iprem] = goal Univ.thy
+val [aprem, iprem] = Goal
     "[| a <= univ(X);                           \
 \       !!i. i:nat ==> a Int Vfrom(X,i) <= b    \
 \    |] ==> a <= b";
@@ -529,7 +546,7 @@
 by (etac iprem 1);
 qed "univ_Int_Vfrom_subset";
 
-val prems = goal Univ.thy
+val prems = Goal
     "[| a <= univ(X);   b <= univ(X);   \
 \       !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \
 \    |] ==> a = b";
@@ -696,3 +713,37 @@
 val FiniteFun_in_univ' = subsetI RSN (2, FiniteFun_in_univ);
 
 
+(**** For QUniv.  Properties of Vfrom analogous to the "take-lemma" ****)
+
+(*** Intersecting a*b with Vfrom... ***)
+
+(*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*)
+Goal "[| {a,b} : Vfrom(X,succ(i));  Transset(X) |]  \
+\     ==> a: Vfrom(X,i)  &  b: Vfrom(X,i)";
+by (dtac (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1);
+by (assume_tac 1);
+by (Fast_tac 1);
+qed "doubleton_in_Vfrom_D";
+
+(*This weaker version says a, b exist at the same level*)
+bind_thm ("Vfrom_doubleton_D", Transset_Vfrom RS Transset_doubleton_D);
+
+(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
+      implies a, b : Vfrom(X,i), which is useless for induction.
+    Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))
+      implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.
+    The combination gives a reduction by precisely one level, which is
+      most convenient for proofs.
+**)
+
+Goalw [Pair_def]
+    "[| <a,b> : Vfrom(X,succ(i));  Transset(X) |]  \
+\    ==> a: Vfrom(X,i)  &  b: Vfrom(X,i)";
+by (blast_tac (claset() addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1);
+qed "Pair_in_Vfrom_D";
+
+Goal "Transset(X) ==>          \
+\      (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))";
+by (blast_tac (claset() addSDs [Pair_in_Vfrom_D]) 1);
+qed "product_Int_Vfrom_subset";
+
diff -r 79b326bceafb -r f8848433d240 src/ZF/WF.ML
--- a/src/ZF/WF.ML	Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/WF.ML	Fri Aug 14 18:37:28 1998 +0200
@@ -48,7 +48,7 @@
 (** Introduction rules for wf_on **)
 
 (*If every non-empty subset of A has an r-minimal element then wf[A](r).*)
-val [prem] = goalw WF.thy [wf_on_def, wf_def]
+val [prem] = Goalw [wf_on_def, wf_def]
     "[| !!Z u. [| Z<=A;  u:Z;  ALL x:Z. EX y:Z. <y,x>:r |] ==> False |] \
 \    ==>  wf[A](r)";
 by (rtac (equals0I RS disjCI RS allI) 1);
@@ -59,7 +59,7 @@
 (*If r allows well-founded induction over A then wf[A](r)
   Premise is equivalent to 
   !!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B  *)
-val [prem] = goal WF.thy
+val [prem] = Goal
     "[| !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A  \
 \              |] ==> y:B |] \
 \    ==>  wf[A](r)";
@@ -74,7 +74,7 @@
 (** Well-founded Induction **)
 
 (*Consider the least z in domain(r) Un {a} such that P(z) does not hold...*)
-val [major,minor] = goalw WF.thy [wf_def]
+val [major,minor] = Goalw [wf_def]
     "[| wf(r);          \
 \       !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x) \
 \    |]  ==>  P(a)";
@@ -92,7 +92,7 @@
            ares_tac prems i];
 
 (*The form of this rule is designed to match wfI*)
-val wfr::amem::prems = goal WF.thy
+val wfr::amem::prems = Goal
     "[| wf(r);  a:A;  field(r)<=A;  \
 \       !!x.[| x: A;  ALL y. <y,x>: r --> P(y) |] ==> P(x) \
 \    |]  ==>  P(a)";
@@ -103,11 +103,11 @@
 by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
 qed "wf_induct2";
 
-goal domrange.thy "!!r A. field(r Int A*A) <= A";
+Goal "!!r A. field(r Int A*A) <= A";
 by (Blast_tac 1);
 qed "field_Int_square";
 
-val wfr::amem::prems = goalw WF.thy [wf_on_def]
+val wfr::amem::prems = Goalw [wf_on_def]
     "[| wf[A](r);  a:A;                                         \
 \       !!x.[| x: A;  ALL y:A. <y,x>: r --> P(y) |] ==> P(x)    \
 \    |]  ==>  P(a)";
@@ -122,7 +122,7 @@
            REPEAT (ares_tac prems i)];
 
 (*If r allows well-founded induction then wf(r)*)
-val [subs,indhyp] = goal WF.thy
+val [subs,indhyp] = Goal
     "[| field(r)<=A;  \
 \       !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A  \
 \              |] ==> y:B |] \
@@ -197,9 +197,8 @@
 
 (** is_recfun **)
 
-val [major] = goalw WF.thy [is_recfun_def]
-    "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)";
-by (stac major 1);
+Goalw [is_recfun_def] "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)";
+by (etac ssubst 1);
 by (rtac (lamI RS rangeI RS lam_type) 1);
 by (assume_tac 1);
 qed "is_recfun_type";
@@ -245,26 +244,22 @@
 
 (*** Main Existence Lemma ***)
 
-val prems = goal WF.thy
-    "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |]  ==>  f=g";
-by (cut_facts_tac prems 1);
+Goal "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |]  ==>  f=g";
 by (rtac fun_extension 1);
 by (REPEAT (ares_tac [is_recfun_equal] 1
      ORELSE eresolve_tac [is_recfun_type,underD] 1));
 qed "is_recfun_functional";
 
 (*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *)
-val prems = goalw WF.thy [the_recfun_def]
+Goalw [the_recfun_def]
     "[| is_recfun(r,a,H,f);  wf(r);  trans(r) |]  \
 \    ==> is_recfun(r, a, H, the_recfun(r,a,H))";
 by (rtac (ex1I RS theI) 1);
-by (REPEAT (ares_tac (prems@[is_recfun_functional]) 1));
+by (REPEAT (ares_tac [is_recfun_functional] 1));
 qed "is_the_recfun";
 
-val prems = goal WF.thy
-    "[| wf(r);  trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))";
-by (cut_facts_tac prems 1);
-by (wf_ind_tac "a" prems 1);
+Goal "[| wf(r);  trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))";
+by (wf_ind_tac "a" [] 1);
 by (res_inst_tac [("f", "lam y: r-``{a1}. wftrec(r,y,H)")] is_the_recfun 1);
 by (REPEAT (assume_tac 2));
 by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
@@ -309,14 +304,14 @@
 qed "wfrec";
 
 (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
-val rew::prems = goal WF.thy
+val rew::prems = Goal
     "[| !!x. h(x)==wfrec(r,x,H);  wf(r) |] ==> \
 \    h(a) = H(a, lam x: r-``{a}. h(x))";
 by (rewtac rew);
 by (REPEAT (resolve_tac (prems@[wfrec]) 1));
 qed "def_wfrec";
 
-val prems = goal WF.thy
+val prems = Goal
     "[| wf(r);  a:A;  field(r)<=A;  \
 \       !!x u. [| x: A;  u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x)   \
 \    |] ==> wfrec(r,a,H) : B(a)";
diff -r 79b326bceafb -r f8848433d240 src/ZF/Zorn.ML
--- a/src/ZF/Zorn.ML	Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/Zorn.ML	Fri Aug 14 18:37:28 1998 +0200
@@ -13,11 +13,11 @@
 
 (*** Section 1.  Mathematical Preamble ***)
 
-goal ZF.thy "!!A B C. (ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
+Goal "!!A B C. (ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
 by (Blast_tac 1);
 qed "Union_lemma0";
 
-goal ZF.thy
+Goal
     "!!A B C. [| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B";
 by (Blast_tac 1);
 qed "Inter_lemma0";
@@ -45,7 +45,7 @@
 
 (** Structural induction on TFin(S,next) **)
 
-val major::prems = goal Zorn.thy
+val major::prems = Goal
   "[| n: TFin(S,next);  \
 \     !!x. [| x : TFin(S,next);  P(x);  next: increasing(S) |] ==> P(next`x); \
 \     !!Y. [| Y <= TFin(S,next);  ALL y:Y. P(y) |] ==> P(Union(Y)) \
@@ -67,12 +67,10 @@
           TFin_is_subset RSN (3, increasingD2 RSN (2,subset_trans)));
 
 (*Lemma 1 of section 3.1*)
-val major::prems = goal Zorn.thy
-    "[| n: TFin(S,next);  m: TFin(S,next);  \
-\       ALL x: TFin(S,next) . x<=m --> x=m | next`x<=m \
-\    |] ==> n<=m | next`m<=n";
-by (cut_facts_tac prems 1);
-by (rtac (major RS TFin_induct) 1);
+Goal "[| n: TFin(S,next);  m: TFin(S,next);  \
+\        ALL x: TFin(S,next) . x<=m --> x=m | next`x<=m \
+\     |] ==> n<=m | next`m<=n";
+by (etac TFin_induct 1);
 by (etac Union_lemma0 2);               (*or just Blast_tac*)
 by (blast_tac (subset_cs addIs [increasing_trans]) 1);
 qed "TFin_linear_lemma1";
@@ -123,10 +121,8 @@
 
 
 (*Lemma 3 of section 3.3*)
-val major::prems = goal Zorn.thy
-    "[| n: TFin(S,next);  m: TFin(S,next);  m = next`m |] ==> n<=m";
-by (cut_facts_tac prems 1);
-by (rtac (major RS TFin_induct) 1);
+Goal "[| n: TFin(S,next);  m: TFin(S,next);  m = next`m |] ==> n<=m";
+by (etac TFin_induct 1);
 by (dtac TFin_subsetD 1);
 by (REPEAT (assume_tac 1));
 by (fast_tac (claset() addEs [ssubst]) 1);
@@ -276,11 +272,10 @@
 (*** Section 6.  Zermelo's Theorem: every set can be well-ordered ***)
 
 (*Lemma 5*)
-val major::prems = goal Zorn.thy
+Goal
     "[| n: TFin(S,next);  Z <= TFin(S,next);  z:Z;  ~ Inter(Z) : Z      \
 \    |] ==> ALL m:Z. n<=m";
-by (cut_facts_tac prems 1);
-by (rtac (major RS TFin_induct) 1);
+by (etac TFin_induct 1);
 by (Blast_tac 2);                  (*second induction step is easy*)
 by (rtac ballI 1);
 by (rtac (bspec RS TFin_subsetD RS disjE) 1);
@@ -324,13 +319,6 @@
 
 (** Defining the "next" operation for Zermelo's Theorem **)
 
-goal AC.thy
-    "!!S. [| ch : (PROD X:Pow(S) - {0}. X);  X<=S;  X~=S        \
-\         |] ==> ch ` (S-X) : S-X";
-by (etac apply_type 1);
-by (blast_tac (claset() addSEs [equalityE]) 1);
-qed "choice_Diff";
-
 (*This justifies Definition 6.1*)
 Goal "ch: (PROD X: Pow(S)-{0}. X) ==>               \
 \          EX next: increasing(S). ALL X: Pow(S).       \
diff -r 79b326bceafb -r f8848433d240 src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/equalities.ML	Fri Aug 14 18:37:28 1998 +0200
@@ -10,23 +10,23 @@
 (** Finite Sets **)
 
 (* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
-goal ZF.thy "{a} Un B = cons(a,B)";
+Goal "{a} Un B = cons(a,B)";
 by (Blast_tac 1);
 qed "cons_eq";
 
-goal ZF.thy "cons(a, cons(b, C)) = cons(b, cons(a, C))";
+Goal "cons(a, cons(b, C)) = cons(b, cons(a, C))";
 by (Blast_tac 1);
 qed "cons_commute";
 
-goal ZF.thy "!!B. a: B ==> cons(a,B) = B";
+Goal "a: B ==> cons(a,B) = B";
 by (Blast_tac 1);
 qed "cons_absorb";
 
-goal ZF.thy "!!B. a: B ==> cons(a, B-{a}) = B";
+Goal "a: B ==> cons(a, B-{a}) = B";
 by (Blast_tac 1);
 qed "cons_Diff";
 
-goal ZF.thy "!!C. [| a: C;  ALL y:C. y=b |] ==> C = {b}";
+Goal "[| a: C;  ALL y:C. y=b |] ==> C = {b}";
 by (Blast_tac 1);
 qed "equal_singleton_lemma";
 val equal_singleton = ballI RSN (2,equal_singleton_lemma);
@@ -35,150 +35,150 @@
 (** Binary Intersection **)
 
 (*NOT an equality, but it seems to belong here...*)
-goal ZF.thy "cons(a,B) Int C <= cons(a, B Int C)";
+Goal "cons(a,B) Int C <= cons(a, B Int C)";
 by (Blast_tac 1);
 qed "Int_cons";
 
-goal ZF.thy "A Int A = A";
+Goal "A Int A = A";
 by (Blast_tac 1);
 qed "Int_absorb";
 
-goal ZF.thy "A Int B = B Int A";
+Goal "A Int B = B Int A";
 by (Blast_tac 1);
 qed "Int_commute";
 
-goal ZF.thy "(A Int B) Int C  =  A Int (B Int C)";
+Goal "(A Int B) Int C  =  A Int (B Int C)";
 by (Blast_tac 1);
 qed "Int_assoc";
 
-goal ZF.thy "(A Un B) Int C  =  (A Int C) Un (B Int C)";
+Goal "(A Un B) Int C  =  (A Int C) Un (B Int C)";
 by (Blast_tac 1);
 qed "Int_Un_distrib";
 
-goal ZF.thy "A<=B <-> A Int B = A";
+Goal "A<=B <-> A Int B = A";
 by (blast_tac (claset() addSEs [equalityE]) 1);
 qed "subset_Int_iff";
 
-goal ZF.thy "A<=B <-> B Int A = A";
+Goal "A<=B <-> B Int A = A";
 by (blast_tac (claset() addSEs [equalityE]) 1);
 qed "subset_Int_iff2";
 
-goal ZF.thy "!!A B C. C<=A ==> (A-B) Int C = C-B";
+Goal "C<=A ==> (A-B) Int C = C-B";
 by (Blast_tac 1);
 qed "Int_Diff_eq";
 
 (** Binary Union **)
 
-goal ZF.thy "cons(a,B) Un C = cons(a, B Un C)";
+Goal "cons(a,B) Un C = cons(a, B Un C)";
 by (Blast_tac 1);
 qed "Un_cons";
 
-goal ZF.thy "A Un A = A";
+Goal "A Un A = A";
 by (Blast_tac 1);
 qed "Un_absorb";
 
-goal ZF.thy "A Un B = B Un A";
+Goal "A Un B = B Un A";
 by (Blast_tac 1);
 qed "Un_commute";
 
-goal ZF.thy "(A Un B) Un C  =  A Un (B Un C)";
+Goal "(A Un B) Un C  =  A Un (B Un C)";
 by (Blast_tac 1);
 qed "Un_assoc";
 
-goal ZF.thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
+Goal "(A Int B) Un C  =  (A Un C) Int (B Un C)";
 by (Blast_tac 1);
 qed "Un_Int_distrib";
 
-goal ZF.thy "A<=B <-> A Un B = B";
+Goal "A<=B <-> A Un B = B";
 by (blast_tac (claset() addSEs [equalityE]) 1);
 qed "subset_Un_iff";
 
-goal ZF.thy "A<=B <-> B Un A = B";
+Goal "A<=B <-> B Un A = B";
 by (blast_tac (claset() addSEs [equalityE]) 1);
 qed "subset_Un_iff2";
 
 (** Simple properties of Diff -- set difference **)
 
-goal ZF.thy "A-A = 0";
+Goal "A-A = 0";
 by (Blast_tac 1);
 qed "Diff_cancel";
 
-goal ZF.thy "0-A = 0";
+Goal "0-A = 0";
 by (Blast_tac 1);
 qed "empty_Diff";
 
-goal ZF.thy "A-0 = A";
+Goal "A-0 = A";
 by (Blast_tac 1);
 qed "Diff_0";
 
-goal ZF.thy "A-B=0 <-> A<=B";
+Goal "A-B=0 <-> A<=B";
 by (blast_tac (claset() addEs [equalityE]) 1);
 qed "Diff_eq_0_iff";
 
 (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
-goal ZF.thy "A - cons(a,B) = A - B - {a}";
+Goal "A - cons(a,B) = A - B - {a}";
 by (Blast_tac 1);
 qed "Diff_cons";
 
 (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
-goal ZF.thy "A - cons(a,B) = A - {a} - B";
+Goal "A - cons(a,B) = A - {a} - B";
 by (Blast_tac 1);
 qed "Diff_cons2";
 
-goal ZF.thy "A Int (B-A) = 0";
+Goal "A Int (B-A) = 0";
 by (Blast_tac 1);
 qed "Diff_disjoint";
 
-goal ZF.thy "!!A B. A<=B ==> A Un (B-A) = B";
+Goal "A<=B ==> A Un (B-A) = B";
 by (Blast_tac 1);
 qed "Diff_partition";
 
-goal ZF.thy "A <= B Un (A - B)";
+Goal "A <= B Un (A - B)";
 by (Blast_tac 1);
 qed "subset_Un_Diff";
 
-goal ZF.thy "!!A B. [| A<=B; B<=C |] ==> B-(C-A) = A";
+Goal "[| A<=B; B<=C |] ==> B-(C-A) = A";
 by (Blast_tac 1);
 qed "double_complement";
 
-goal ZF.thy "(A Un B) - (B-A) = A";
+Goal "(A Un B) - (B-A) = A";
 by (Blast_tac 1);
 qed "double_complement_Un";
 
-goal ZF.thy
+Goal
  "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
 by (Blast_tac 1);
 qed "Un_Int_crazy";
 
-goal ZF.thy "A - (B Un C) = (A-B) Int (A-C)";
+Goal "A - (B Un C) = (A-B) Int (A-C)";
 by (Blast_tac 1);
 qed "Diff_Un";
 
-goal ZF.thy "A - (B Int C) = (A-B) Un (A-C)";
+Goal "A - (B Int C) = (A-B) Un (A-C)";
 by (Blast_tac 1);
 qed "Diff_Int";
 
 (*Halmos, Naive Set Theory, page 16.*)
-goal ZF.thy "(A Int B) Un C = A Int (B Un C)  <->  C<=A";
+Goal "(A Int B) Un C = A Int (B Un C)  <->  C<=A";
 by (blast_tac (claset() addSEs [equalityE]) 1);
 qed "Un_Int_assoc_iff";
 
 
 (** Big Union and Intersection **)
 
-goal ZF.thy "Union(cons(a,B)) = a Un Union(B)";
+Goal "Union(cons(a,B)) = a Un Union(B)";
 by (Blast_tac 1);
 qed "Union_cons";
 
-goal ZF.thy "Union(A Un B) = Union(A) Un Union(B)";
+Goal "Union(A Un B) = Union(A) Un Union(B)";
 by (Blast_tac 1);
 qed "Union_Un_distrib";
 
-goal ZF.thy "Union(A Int B) <= Union(A) Int Union(B)";
+Goal "Union(A Int B) <= Union(A) Int Union(B)";
 by (Blast_tac 1);
 qed "Union_Int_subset";
 
-goal ZF.thy "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)";
+Goal "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)";
 by (blast_tac (claset() addSEs [equalityE]) 1);
 qed "Union_disjoint";
 
@@ -186,26 +186,26 @@
 by (Blast_tac 1);
 qed "Inter_0";
 
-goal ZF.thy "!!A B. [| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)";
+Goal "[| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)";
 by (Blast_tac 1);
 qed "Inter_Un_subset";
 
 (* A good challenge: Inter is ill-behaved on the empty set *)
-goal ZF.thy "!!A B. [| a:A;  b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)";
+Goal "[| a:A;  b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)";
 by (Blast_tac 1);
 qed "Inter_Un_distrib";
 
-goal ZF.thy "Union({b}) = b";
+Goal "Union({b}) = b";
 by (Blast_tac 1);
 qed "Union_singleton";
 
-goal ZF.thy "Inter({b}) = b";
+Goal "Inter({b}) = b";
 by (Blast_tac 1);
 qed "Inter_singleton";
 
 (** Unions and Intersections of Families **)
 
-goal ZF.thy "Union(A) = (UN x:A. x)";
+Goal "Union(A) = (UN x:A. x)";
 by (Blast_tac 1);
 qed "Union_eq_UN";
 
@@ -213,43 +213,41 @@
 by (Blast_tac 1);
 qed "Inter_eq_INT";
 
-goal ZF.thy "(UN i:0. A(i)) = 0";
+Goal "(UN i:0. A(i)) = 0";
 by (Blast_tac 1);
 qed "UN_0";
 
 (*Halmos, Naive Set Theory, page 35.*)
-goal ZF.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
+Goal "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
 by (Blast_tac 1);
 qed "Int_UN_distrib";
 
-goal ZF.thy "!!A B. i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
+Goal "i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
 by (Blast_tac 1);
 qed "Un_INT_distrib";
 
-goal ZF.thy
-    "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
+Goal "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
 by (Blast_tac 1);
 qed "Int_UN_distrib2";
 
-goal ZF.thy
-    "!!I J. [| i:I;  j:J |] ==> \
-\    (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
+Goal "[| i:I;  j:J |] ==> \
+\     (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
 by (Blast_tac 1);
 qed "Un_INT_distrib2";
 
-goal ZF.thy "!!A. a: A ==> (UN y:A. c) = c";
+Goal "a: A ==> (UN y:A. c) = c";
 by (Blast_tac 1);
 qed "UN_constant";
 
-goal ZF.thy "!!A. a: A ==> (INT y:A. c) = c";
+Goal "a: A ==> (INT y:A. c) = c";
 by (Blast_tac 1);
 qed "INT_constant";
 
-goal ZF.thy "(UN y: RepFun(A,f). B(y)) = (UN x:A. B(f(x)))";
+Goal "(UN y: RepFun(A,f). B(y)) = (UN x:A. B(f(x)))";
 by (Blast_tac 1);
 qed "UN_RepFun";
 
-goal ZF.thy "!!x. x:A ==> (INT y: RepFun(A,f). B(y)) = (INT x:A. B(f(x)))";
+Goal "x:A ==> (INT y: RepFun(A,f). B(y)) = (INT x:A. B(f(x)))";
 by (Blast_tac 1);
 qed "INT_RepFun";
 
@@ -259,94 +257,92 @@
 (** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
     Union of a family of unions **)
 
-goal ZF.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
+Goal "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
 by (Blast_tac 1);
 qed "UN_Un_distrib";
 
-goal ZF.thy
-    "!!A B. i:I ==> \
-\           (INT i:I. A(i)  Int  B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
+Goal "i:I ==> (INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
 by (Blast_tac 1);
 qed "INT_Int_distrib";
 
-goal ZF.thy "(UN z:I Int J. A(z)) <= (UN z:I. A(z)) Int (UN z:J. A(z))";
+Goal "(UN z:I Int J. A(z)) <= (UN z:I. A(z)) Int (UN z:J. A(z))";
 by (Blast_tac 1);
 qed "UN_Int_subset";
 
 (** Devlin, page 12, exercise 5: Complements **)
 
-goal ZF.thy "!!A B. i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))";
+Goal "i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))";
 by (Blast_tac 1);
 qed "Diff_UN";
 
-goal ZF.thy "!!A B. i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))";
+Goal "i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))";
 by (Blast_tac 1);
 qed "Diff_INT";
 
 (** Unions and Intersections with General Sum **)
 
 (*Not suitable for rewriting: LOOPS!*)
-goal ZF.thy "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)";
+Goal "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)";
 by (Blast_tac 1);
 qed "Sigma_cons1";
 
 (*Not suitable for rewriting: LOOPS!*)
-goal ZF.thy "A * cons(b,B) = A*{b} Un A*B";
+Goal "A * cons(b,B) = A*{b} Un A*B";
 by (Blast_tac 1);
 qed "Sigma_cons2";
 
-goal ZF.thy "Sigma(succ(A), B) = ({A}*B(A)) Un Sigma(A,B)";
+Goal "Sigma(succ(A), B) = ({A}*B(A)) Un Sigma(A,B)";
 by (Blast_tac 1);
 qed "Sigma_succ1";
 
-goal ZF.thy "A * succ(B) = A*{B} Un A*B";
+Goal "A * succ(B) = A*{B} Un A*B";
 by (Blast_tac 1);
 qed "Sigma_succ2";
 
-goal ZF.thy "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))";
+Goal "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))";
 by (Blast_tac 1);
 qed "SUM_UN_distrib1";
 
-goal ZF.thy "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))";
+Goal "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))";
 by (Blast_tac 1);
 qed "SUM_UN_distrib2";
 
-goal ZF.thy "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))";
+Goal "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))";
 by (Blast_tac 1);
 qed "SUM_Un_distrib1";
 
-goal ZF.thy "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))";
+Goal "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))";
 by (Blast_tac 1);
 qed "SUM_Un_distrib2";
 
 (*First-order version of the above, for rewriting*)
-goal ZF.thy "I * (A Un B) = I*A Un I*B";
+Goal "I * (A Un B) = I*A Un I*B";
 by (rtac SUM_Un_distrib2 1);
 qed "prod_Un_distrib2";
 
-goal ZF.thy "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))";
+Goal "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))";
 by (Blast_tac 1);
 qed "SUM_Int_distrib1";
 
-goal ZF.thy
-    "(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))";
+Goal "(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))";
 by (Blast_tac 1);
 qed "SUM_Int_distrib2";
 
 (*First-order version of the above, for rewriting*)
-goal ZF.thy "I * (A Int B) = I*A Int I*B";
+Goal "I * (A Int B) = I*A Int I*B";
 by (rtac SUM_Int_distrib2 1);
 qed "prod_Int_distrib2";
 
 (*Cf Aczel, Non-Well-Founded Sets, page 115*)
-goal ZF.thy "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))";
+Goal "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))";
 by (Blast_tac 1);
 qed "SUM_eq_UN";
 
 (** Domain **)
 
-qed_goal "domain_of_prod" ZF.thy "!!A B. b:B ==> domain(A*B) = A"
- (fn _ => [ Blast_tac 1 ]);
+Goal "b:B ==> domain(A*B) = A";
+by (Blast_tac 1);
+qed "domain_of_prod";
 
 qed_goal "domain_0" ZF.thy "domain(0) = 0"
  (fn _ => [ Blast_tac 1 ]);
@@ -355,19 +351,19 @@
     "domain(cons(<a,b>,r)) = cons(a, domain(r))"
  (fn _ => [ Blast_tac 1 ]);
 
-goal ZF.thy "domain(A Un B) = domain(A) Un domain(B)";
+Goal "domain(A Un B) = domain(A) Un domain(B)";
 by (Blast_tac 1);
 qed "domain_Un_eq";
 
-goal ZF.thy "domain(A Int B) <= domain(A) Int domain(B)";
+Goal "domain(A Int B) <= domain(A) Int domain(B)";
 by (Blast_tac 1);
 qed "domain_Int_subset";
 
-goal ZF.thy "domain(A) - domain(B) <= domain(A - B)";
+Goal "domain(A) - domain(B) <= domain(A - B)";
 by (Blast_tac 1);
 qed "domain_Diff_subset";
 
-goal ZF.thy "domain(converse(r)) = range(r)";
+Goal "domain(converse(r)) = range(r)";
 by (Blast_tac 1);
 qed "domain_converse";
 
@@ -376,9 +372,9 @@
 
 (** Range **)
 
-qed_goal "range_of_prod" ZF.thy
-    "!!a A B. a:A ==> range(A*B) = B"
- (fn _ => [ Blast_tac 1 ]);
+Goal "a:A ==> range(A*B) = B";
+by (Blast_tac 1);
+qed "range_of_prod";
 
 qed_goal "range_0" ZF.thy "range(0) = 0"
  (fn _ => [ Blast_tac 1 ]); 
@@ -387,19 +383,19 @@
     "range(cons(<a,b>,r)) = cons(b, range(r))"
  (fn _ => [ Blast_tac 1 ]);
 
-goal ZF.thy "range(A Un B) = range(A) Un range(B)";
+Goal "range(A Un B) = range(A) Un range(B)";
 by (Blast_tac 1);
 qed "range_Un_eq";
 
-goal ZF.thy "range(A Int B) <= range(A) Int range(B)";
+Goal "range(A Int B) <= range(A) Int range(B)";
 by (Blast_tac 1);
 qed "range_Int_subset";
 
-goal ZF.thy "range(A) - range(B) <= range(A - B)";
+Goal "range(A) - range(B) <= range(A - B)";
 by (Blast_tac 1);
 qed "range_Diff_subset";
 
-goal ZF.thy "range(converse(r)) = domain(r)";
+Goal "range(converse(r)) = domain(r)";
 by (Blast_tac 1);
 qed "range_converse";
 
@@ -418,19 +414,19 @@
     "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
  (fn _ => [ rtac equalityI 1, ALLGOALS (Blast_tac) ]);
 
-goal ZF.thy "field(A Un B) = field(A) Un field(B)";
+Goal "field(A Un B) = field(A) Un field(B)";
 by (Blast_tac 1);
 qed "field_Un_eq";
 
-goal ZF.thy "field(A Int B) <= field(A) Int field(B)";
+Goal "field(A Int B) <= field(A) Int field(B)";
 by (Blast_tac 1);
 qed "field_Int_subset";
 
-goal ZF.thy "field(A) - field(B) <= field(A - B)";
+Goal "field(A) - field(B) <= field(A - B)";
 by (Blast_tac 1);
 qed "field_Diff_subset";
 
-goal ZF.thy "field(converse(r)) = field(r)";
+Goal "field(converse(r)) = field(r)";
 by (Blast_tac 1);
 qed "field_converse";
 
@@ -439,72 +435,74 @@
 
 (** Image **)
 
-goal ZF.thy "r``0 = 0";
+Goal "r``0 = 0";
 by (Blast_tac 1);
 qed "image_0";
 
-goal ZF.thy "r``(A Un B) = (r``A) Un (r``B)";
+Goal "r``(A Un B) = (r``A) Un (r``B)";
 by (Blast_tac 1);
 qed "image_Un";
 
-goal ZF.thy "r``(A Int B) <= (r``A) Int (r``B)";
+Goal "r``(A Int B) <= (r``A) Int (r``B)";
 by (Blast_tac 1);
 qed "image_Int_subset";
 
-goal ZF.thy "(r Int A*A)``B <= (r``B) Int A";
+Goal "(r Int A*A)``B <= (r``B) Int A";
 by (Blast_tac 1);
 qed "image_Int_square_subset";
 
-goal ZF.thy "!!r. B<=A ==> (r Int A*A)``B = (r``B) Int A";
+Goal "B<=A ==> (r Int A*A)``B = (r``B) Int A";
 by (Blast_tac 1);
 qed "image_Int_square";
 
 Addsimps [image_0, image_Un];
 
 (*Image laws for special relations*)
-goal ZF.thy "0``A = 0";
+Goal "0``A = 0";
 by (Blast_tac 1);
 qed "image_0_left";
 Addsimps [image_0_left];
 
-goal ZF.thy "(r Un s)``A = (r``A) Un (s``A)";
+Goal "(r Un s)``A = (r``A) Un (s``A)";
 by (Blast_tac 1);
 qed "image_Un_left";
 
-goal ZF.thy "(r Int s)``A <= (r``A) Int (s``A)";
+Goal "(r Int s)``A <= (r``A) Int (s``A)";
 by (Blast_tac 1);
 qed "image_Int_subset_left";
 
 
 (** Inverse Image **)
 
-goal ZF.thy "r-``0 = 0";
+Goal "r-``0 = 0";
 by (Blast_tac 1);
 qed "vimage_0";
 
-goal ZF.thy "r-``(A Un B) = (r-``A) Un (r-``B)";
+Goal "r-``(A Un B) = (r-``A) Un (r-``B)";
 by (Blast_tac 1);
 qed "vimage_Un";
 
-goal ZF.thy "r-``(A Int B) <= (r-``A) Int (r-``B)";
+Goal "r-``(A Int B) <= (r-``A) Int (r-``B)";
 by (Blast_tac 1);
 qed "vimage_Int_subset";
 
-Goalw [function_def]
-    "function(f) ==> f-``(A Int B) = (f-``A)  Int  (f-``B)";
+Goalw [function_def] "function(f) ==> f-``(A Int B) = (f-``A)  Int  (f-``B)";
 by (Blast_tac 1);
 qed "function_vimage_Int";
 
-Goalw [function_def]
-    "function(f) ==> f-``(A-B) = (f-``A) - (f-``B)";
+Goalw [function_def] "function(f) ==> f-``(A-B) = (f-``A) - (f-``B)";
 by (Blast_tac 1);
 qed "function_vimage_Diff";
 
-goal ZF.thy "(r Int A*A)-``B <= (r-``B) Int A";
+Goalw [function_def] "function(f) ==> f `` (f-`` A) <= A";
+by (Blast_tac 1);
+qed "function_image_vimage";
+
+Goal "(r Int A*A)-``B <= (r-``B) Int A";
 by (Blast_tac 1);
 qed "vimage_Int_square_subset";
 
-goal ZF.thy "!!r. B<=A ==> (r Int A*A)-``B = (r-``B) Int A";
+Goal "B<=A ==> (r Int A*A)-``B = (r-``B) Int A";
 by (Blast_tac 1);
 qed "vimage_Int_square";
 
@@ -512,35 +510,35 @@
 
 
 (*Invese image laws for special relations*)
-goal ZF.thy "0-``A = 0";
+Goal "0-``A = 0";
 by (Blast_tac 1);
 qed "vimage_0_left";
 Addsimps [vimage_0_left];
 
-goal ZF.thy "(r Un s)-``A = (r-``A) Un (s-``A)";
+Goal "(r Un s)-``A = (r-``A) Un (s-``A)";
 by (Blast_tac 1);
 qed "vimage_Un_left";
 
-goal ZF.thy "(r Int s)-``A <= (r-``A) Int (s-``A)";
+Goal "(r Int s)-``A <= (r-``A) Int (s-``A)";
 by (Blast_tac 1);
 qed "vimage_Int_subset_left";
 
 
 (** Converse **)
 
-goal ZF.thy "converse(A Un B) = converse(A) Un converse(B)";
+Goal "converse(A Un B) = converse(A) Un converse(B)";
 by (Blast_tac 1);
 qed "converse_Un";
 
-goal ZF.thy "converse(A Int B) = converse(A) Int converse(B)";
+Goal "converse(A Int B) = converse(A) Int converse(B)";
 by (Blast_tac 1);
 qed "converse_Int";
 
-goal ZF.thy "converse(A - B) = converse(A) - converse(B)";
+Goal "converse(A - B) = converse(A) - converse(B)";
 by (Blast_tac 1);
 qed "converse_Diff";
 
-goal ZF.thy "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))";
+Goal "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))";
 by (Blast_tac 1);
 qed "converse_UN";
 
@@ -553,27 +551,27 @@
 
 (** Pow **)
 
-goal ZF.thy "Pow(A) Un Pow(B) <= Pow(A Un B)";
+Goal "Pow(A) Un Pow(B) <= Pow(A Un B)";
 by (Blast_tac 1);
 qed "Un_Pow_subset";
 
-goal ZF.thy "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))";
+Goal "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))";
 by (Blast_tac 1);
 qed "UN_Pow_subset";
 
-goal ZF.thy "A <= Pow(Union(A))";
+Goal "A <= Pow(Union(A))";
 by (Blast_tac 1);
 qed "subset_Pow_Union";
 
-goal ZF.thy "Union(Pow(A)) = A";
+Goal "Union(Pow(A)) = A";
 by (Blast_tac 1);
 qed "Union_Pow_eq";
 
-goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
+Goal "Pow(A Int B) = Pow(A) Int Pow(B)";
 by (Blast_tac 1);
 qed "Int_Pow_eq";
 
-goal ZF.thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
+Goal "x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
 by (Blast_tac 1);
 qed "INT_Pow_subset";
 
@@ -581,26 +579,26 @@
 
 (** RepFun **)
 
-goal ZF.thy "{f(x).x:A}=0 <-> A=0";
+Goal "{f(x).x:A}=0 <-> A=0";
 	(*blast_tac takes too long to find a good depth*)
 by (Blast.depth_tac (claset() addSEs [equalityE]) 10 1);
 qed "RepFun_eq_0_iff";
 
 (** Collect **)
 
-goal ZF.thy "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)";
+Goal "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)";
 by (Blast_tac 1);
 qed "Collect_Un";
 
-goal ZF.thy "Collect(A Int B, P) = Collect(A,P) Int Collect(B,P)";
+Goal "Collect(A Int B, P) = Collect(A,P) Int Collect(B,P)";
 by (Blast_tac 1);
 qed "Collect_Int";
 
-goal ZF.thy "Collect(A - B, P) = Collect(A,P) - Collect(B,P)";
+Goal "Collect(A - B, P) = Collect(A,P) - Collect(B,P)";
 by (Blast_tac 1);
 qed "Collect_Diff";
 
-goal ZF.thy "{x:cons(a,B). P(x)} = if(P(a), cons(a, {x:B. P(x)}), {x:B. P(x)})";
+Goal "{x:cons(a,B). P(x)} = if(P(a), cons(a, {x:B. P(x)}), {x:B. P(x)})";
 by (simp_tac (simpset() addsplits [split_if]) 1);
 by (Blast_tac 1);
 qed "Collect_cons";
diff -r 79b326bceafb -r f8848433d240 src/ZF/func.ML
--- a/src/ZF/func.ML	Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/func.ML	Fri Aug 14 18:37:28 1998 +0200
@@ -389,25 +389,23 @@
 
 (*** Extensions of functions ***)
 
-goal ZF.thy
-    "!!f A B. [| f: A->B;  c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
+Goal "[| f: A->B;  c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
 by (forward_tac [singleton_fun RS fun_disjoint_Un] 1);
 by (asm_full_simp_tac (FOL_ss addsimps [cons_eq]) 2);
 by (Blast_tac 1);
 qed "fun_extend";
 
-goal ZF.thy
-    "!!f A B. [| f: A->B;  c~:A;  b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B";
+Goal "[| f: A->B;  c~:A;  b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B";
 by (blast_tac (claset() addIs [fun_extend RS fun_weaken_type]) 1);
 qed "fun_extend3";
 
-goal ZF.thy "!!f A B. [| f: A->B;  a:A;  c~:A |] ==> cons(<c,b>,f)`a = f`a";
+Goal "[| f: A->B;  a:A;  c~:A |] ==> cons(<c,b>,f)`a = f`a";
 by (rtac (apply_Pair RS consI2 RS apply_equality) 1);
 by (rtac fun_extend 3);
 by (REPEAT (assume_tac 1));
 qed "fun_extend_apply1";
 
-goal ZF.thy "!!f A B. [| f: A->B;  c~:A |] ==> cons(<c,b>,f)`c = b";
+Goal "[| f: A->B;  c~:A |] ==> cons(<c,b>,f)`c = b";
 by (rtac (consI1 RS apply_equality) 1);
 by (rtac fun_extend 1);
 by (REPEAT (assume_tac 1));
@@ -417,8 +415,7 @@
 Addsimps [singleton_apply];
 
 (*For Finite.ML.  Inclusion of right into left is easy*)
-goal ZF.thy
-    "!!c. c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})";
+Goal "c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})";
 by (rtac equalityI 1);
 by (safe_tac (claset() addSEs [fun_extend3]));
 (*Inclusion of left into right*)