# HG changeset patch
# User paulson
# Date 903352148 -7200
# Node ID f7a5e06adea1c09e649e07118eee8d84666dcf44
# Parent  ec84178243ffc6e88b9b20b96906afe6bc6aa949
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
contains fewer theorems than before

diff -r ec84178243ff -r f7a5e06adea1 src/ZF/AC/AC7_AC9.ML
--- a/src/ZF/AC/AC7_AC9.ML	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/AC/AC7_AC9.ML	Mon Aug 17 13:09:08 1998 +0200
@@ -13,13 +13,10 @@
 (*  - Sigma_fun_space_eqpoll                                              *)
 (* ********************************************************************** *)
 
-goal ZF.thy "!!A. [| C~:A; B:A |] ==> B~=C";
-by (Fast_tac 1);
-qed "mem_not_eq_not_mem";
-
 Goal "[| 0~:A; B:A |] ==> (nat->Union(A))*B ~= 0";
-by (blast_tac (claset() addSDs [Sigma_empty_iff RS iffD1]
-                addDs [fun_space_emptyD, mem_not_eq_not_mem]) 1);
+by (blast_tac (claset() addSDs [Sigma_empty_iff RS iffD1, 
+				Union_empty_iff RS iffD1]
+                        addDs [fun_space_emptyD]) 1);
 qed "Sigma_fun_space_not0";
 
 Goal "(ALL B:A. B eqpoll C) ==> (ALL B1:A. ALL B2:A. B1 eqpoll B2)";
diff -r ec84178243ff -r f7a5e06adea1 src/ZF/AC/AC_Equiv.ML
--- a/src/ZF/AC/AC_Equiv.ML	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/AC/AC_Equiv.ML	Mon Aug 17 13:09:08 1998 +0200
@@ -44,8 +44,7 @@
 
 (* used only in WO1_DC.ML *)
 (*Note simpler proof*)
-goal ZF.thy "!!A f g. [| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg;  \
-\         A<=Df; A<=Dg |] ==> f``A=g``A";
+Goal "[| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; A<=Df; A<=Dg |] ==> f``A=g``A";
 by (asm_simp_tac (simpset() addsimps [image_fun]) 1);
 qed "images_eq";
 
diff -r ec84178243ff -r f7a5e06adea1 src/ZF/AC/WO6_WO1.ML
--- a/src/ZF/AC/WO6_WO1.ML	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/AC/WO6_WO1.ML	Mon Aug 17 13:09:08 1998 +0200
@@ -172,9 +172,8 @@
 by (fast_tac (claset() addSEs [LeastI, lt_Ord]) 1);
 qed "uu_not_empty";
 
-goal ZF.thy "!!r. [| r<=A*B; r~=0 |] ==> domain(r)~=0";
-by (REPEAT (eresolve_tac [asm_rl, not_emptyE, subsetD RS SigmaE, 
-                sym RSN (2, subst_elem) RS domainI RS not_emptyI] 1));
+Goal "[| r<=A*B; r~=0 |] ==> domain(r)~=0";
+by (Blast_tac 1);
 qed "not_empty_rel_imp_domain";
 
 Goal "[| b<a; g<a; f`b~=0; f`g~=0;  \
@@ -186,7 +185,7 @@
         THEN (REPEAT (ares_tac [lt_Ord] 1)));
 qed "Least_uu_not_empty_lt_a";
 
-goal ZF.thy "!!B. [| B<=A; a~:B |] ==> B <= A-{a}";
+Goal "[| B<=A; a~:B |] ==> B <= A-{a}";
 by (Blast_tac 1);
 qed "subset_Diff_sing";
 
@@ -194,14 +193,11 @@
 Goal "[| A lepoll m; m lepoll B; B <= A; m:nat |] ==> A=B";
 by (etac natE 1);
 by (fast_tac (claset() addSDs [lepoll_0_is_0] addSIs [equalityI]) 1);
-by (hyp_subst_tac 1);
-by (rtac equalityI 1);
-by (assume_tac 2);
-by (rtac subsetI 1);
-by (excluded_middle_tac "?P" 1 THEN (assume_tac 2));
-by (eresolve_tac [subset_Diff_sing RS subset_imp_lepoll RSN (2, 
-                Diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS 
-                succ_lepoll_natE] 1
+by (safe_tac (claset() addSIs [equalityI])); 
+by (rtac ccontr 1);
+by (etac (subset_Diff_sing RS subset_imp_lepoll 
+	  RSN (2, Diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS 
+	  succ_lepoll_natE) 1
         THEN REPEAT (assume_tac 1));
 qed "supset_lepoll_imp_eq";
 
diff -r ec84178243ff -r f7a5e06adea1 src/ZF/Arith.ML
--- a/src/ZF/Arith.ML	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/Arith.ML	Mon Aug 17 13:09:08 1998 +0200
@@ -34,7 +34,7 @@
 
 Addsimps [rec_0, rec_succ];
 
-val major::prems = goal Arith.thy
+val major::prems = Goal
     "[| n: nat;  \
 \       a: C(0);  \
 \       !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m))  \
@@ -467,7 +467,7 @@
 qed "add_lt_mono";
 
 (*A [clumsy] way of lifting < monotonicity to le monotonicity *)
-val lt_mono::ford::prems = goal Ordinal.thy
+val lt_mono::ford::prems = Goal
      "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j); \
 \        !!i. i:k ==> Ord(f(i));                \
 \        i le j;  j:k                           \
diff -r ec84178243ff -r f7a5e06adea1 src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/Cardinal.ML	Mon Aug 17 13:09:08 1998 +0200
@@ -29,16 +29,15 @@
                              gfun RS fun_is_rel RS image_subset]) 1);
 qed "Banach_last_equation";
 
-val prems = goal Cardinal.thy
-    "[| f: X->Y;  g: Y->X |] ==>   \
-\    EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) &    \
-\                    (YA Int YB = 0) & (YA Un YB = Y) &    \
-\                    f``XA=YA & g``YB=XB";
+Goal "[| f: X->Y;  g: Y->X |] ==>   \
+\     EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) &    \
+\                     (YA Int YB = 0) & (YA Un YB = Y) &    \
+\                     f``XA=YA & g``YB=XB";
 by (REPEAT 
     (FIRSTGOAL
      (resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition])));
 by (rtac Banach_last_equation 3);
-by (REPEAT (resolve_tac (prems@[fun_is_rel, image_subset, lfp_subset]) 1));
+by (REPEAT (ares_tac [fun_is_rel, image_subset, lfp_subset] 1));
 qed "decomposition";
 
 val prems = goal Cardinal.thy
@@ -740,7 +739,7 @@
 (*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered
   set is well-ordered.  Proofs simplified by lcp. *)
 
-goal Nat.thy "!!n. n:nat ==> wf[n](converse(Memrel(n)))";
+Goal "n:nat ==> wf[n](converse(Memrel(n)))";
 by (etac nat_induct 1);
 by (blast_tac (claset() addIs [wf_onI]) 1);
 by (rtac wf_onI 1);
diff -r ec84178243ff -r f7a5e06adea1 src/ZF/CardinalArith.ML
--- a/src/ZF/CardinalArith.ML	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/CardinalArith.ML	Mon Aug 17 13:09:08 1998 +0200
@@ -380,8 +380,8 @@
 (*** An infinite cardinal equals its square (Kunen, Thm 10.12, page 29) ***)
 
 (*A general fact about ordermap*)
-goalw Cardinal.thy [eqpoll_def]
-    "!!A. [| well_ord(A,r);  x:A |] ==> ordermap(A,r)`x eqpoll pred(A,x,r)";
+Goalw [eqpoll_def]
+    "[| well_ord(A,r);  x:A |] ==> ordermap(A,r)`x eqpoll pred(A,x,r)";
 by (rtac exI 1);
 by (asm_simp_tac (simpset() addsimps [ordermap_eq_image, well_ord_is_wf]) 1);
 by (etac (ordermap_bij RS bij_is_inj RS restrict_bij RS bij_converse_bij) 1);
@@ -808,7 +808,3 @@
 		  addsimps [nat_cadd_eq_add RS sym, cadd_def, eqpoll_refl]) 1);
 qed "nat_sum_eqpoll_sum";
 
-goal Nat.thy "!!m. [| m le n; n:nat |] ==> m:nat";
-by (blast_tac (claset() addSDs [lt_nat_in_nat]) 1);
-qed "le_in_nat";
-
diff -r ec84178243ff -r f7a5e06adea1 src/ZF/Nat.ML
--- a/src/ZF/Nat.ML	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/Nat.ML	Mon Aug 17 13:09:08 1998 +0200
@@ -125,6 +125,10 @@
 by (assume_tac 1);
 qed "lt_nat_in_nat";
 
+Goal "[| m le n; n:nat |] ==> m:nat";
+by (blast_tac (claset() addSDs [lt_nat_in_nat]) 1);
+qed "le_in_nat";
+
 
 (** Variations on mathematical induction **)
 
diff -r ec84178243ff -r f7a5e06adea1 src/ZF/Sum.thy
--- a/src/ZF/Sum.thy	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/Sum.thy	Mon Aug 17 13:09:08 1998 +0200
@@ -7,7 +7,7 @@
 "Part" primitive for simultaneous recursive type definitions
 *)
 
-Sum = Bool + pair + 
+Sum = Bool + equalities + 
 
 global
 
diff -r ec84178243ff -r f7a5e06adea1 src/ZF/domrange.ML
--- a/src/ZF/domrange.ML	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/domrange.ML	Mon Aug 17 13:09:08 1998 +0200
@@ -8,19 +8,19 @@
 
 (*** converse ***)
 
-qed_goalw "converse_iff" ZF.thy [converse_def]
+qed_goalw "converse_iff" thy [converse_def]
     "<a,b>: converse(r) <-> <b,a>:r"
  (fn _ => [ (Blast_tac 1) ]);
 
-qed_goalw "converseI" ZF.thy [converse_def]
+qed_goalw "converseI" thy [converse_def]
     "!!a b r. <a,b>:r ==> <b,a>:converse(r)"
  (fn _ => [ (Blast_tac 1) ]);
 
-qed_goalw "converseD" ZF.thy [converse_def]
+qed_goalw "converseD" thy [converse_def]
     "!!a b r. <a,b> : converse(r) ==> <b,a> : r"
  (fn _ => [ (Blast_tac 1) ]);
 
-qed_goalw "converseE" ZF.thy [converse_def]
+qed_goalw "converseE" thy [converse_def]
     "[| yx : converse(r);  \
 \       !!x y. [| yx=<y,x>;  <x,y>:r |] ==> P \
 \    |] ==> P"
@@ -34,36 +34,36 @@
 AddSIs [converseI];
 AddSEs [converseD,converseE];
 
-qed_goal "converse_converse" ZF.thy
+qed_goal "converse_converse" thy
     "!!A B r. r<=Sigma(A,B) ==> converse(converse(r)) = r"
  (fn _ => [ (Blast_tac 1) ]);
 
-qed_goal "converse_type" ZF.thy "!!A B r. r<=A*B ==> converse(r)<=B*A"
+qed_goal "converse_type" thy "!!A B r. r<=A*B ==> converse(r)<=B*A"
  (fn _ => [ (Blast_tac 1) ]);
 
-qed_goal "converse_prod" ZF.thy "converse(A*B) = B*A"
+qed_goal "converse_prod" thy "converse(A*B) = B*A"
  (fn _ => [ (Blast_tac 1) ]);
 
-qed_goal "converse_empty" ZF.thy "converse(0) = 0"
+qed_goal "converse_empty" thy "converse(0) = 0"
  (fn _ => [ (Blast_tac 1) ]);
 
 Addsimps [converse_prod, converse_empty];
 
-val converse_subset_iff = prove_goal ZF.thy
+val converse_subset_iff = prove_goal thy
   "!!z. A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B"
  (fn _=> [ (Blast_tac 1) ]);
 
 
 (*** domain ***)
 
-qed_goalw "domain_iff" ZF.thy [domain_def]
+qed_goalw "domain_iff" thy [domain_def]
     "a: domain(r) <-> (EX y. <a,y>: r)"
  (fn _=> [ (Blast_tac 1) ]);
 
-qed_goal "domainI" ZF.thy "!!a b r. <a,b>: r ==> a: domain(r)"
+qed_goal "domainI" thy "!!a b r. <a,b>: r ==> a: domain(r)"
  (fn _=> [ (etac (exI RS (domain_iff RS iffD2)) 1) ]);
 
-qed_goal "domainE" ZF.thy
+qed_goal "domainE" thy
     "[| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P"
  (fn prems=>
   [ (rtac (domain_iff RS iffD1 RS exE) 1),
@@ -72,15 +72,15 @@
 AddIs  [domainI];
 AddSEs [domainE];
 
-qed_goal "domain_subset" ZF.thy "domain(Sigma(A,B)) <= A"
+qed_goal "domain_subset" thy "domain(Sigma(A,B)) <= A"
  (fn _=> [ (Blast_tac 1) ]);
 
 (*** range ***)
 
-qed_goalw "rangeI" ZF.thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)"
+qed_goalw "rangeI" thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)"
  (fn _ => [ (etac (converseI RS domainI) 1) ]);
 
-qed_goalw "rangeE" ZF.thy [range_def]
+qed_goalw "rangeE" thy [range_def]
     "[| b : range(r);  !!x. <x,b>: r ==> P |] ==> P"
  (fn major::prems=>
   [ (rtac (major RS domainE) 1),
@@ -90,7 +90,7 @@
 AddIs  [rangeI];
 AddSEs [rangeE];
 
-qed_goalw "range_subset" ZF.thy [range_def] "range(A*B) <= B"
+qed_goalw "range_subset" thy [range_def] "range(A*B) <= B"
  (fn _ =>
   [ (stac converse_prod 1),
     (rtac domain_subset 1) ]);
@@ -98,17 +98,17 @@
 
 (*** field ***)
 
-qed_goalw "fieldI1" ZF.thy [field_def] "!!r. <a,b>: r ==> a : field(r)"
+qed_goalw "fieldI1" thy [field_def] "!!r. <a,b>: r ==> a : field(r)"
  (fn _ => [ (Blast_tac 1) ]);
 
-qed_goalw "fieldI2" ZF.thy [field_def] "!!r. <a,b>: r ==> b : field(r)"
+qed_goalw "fieldI2" thy [field_def] "!!r. <a,b>: r ==> b : field(r)"
  (fn _ => [ (Blast_tac 1) ]);
 
-qed_goalw "fieldCI" ZF.thy [field_def]
+qed_goalw "fieldCI" thy [field_def]
     "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"
  (fn [prem]=> [ (blast_tac (claset() addIs [prem]) 1) ]);
 
-qed_goalw "fieldE" ZF.thy [field_def]
+qed_goalw "fieldE" thy [field_def]
      "[| a : field(r);  \
 \        !!x. <a,x>: r ==> P;  \
 \        !!x. <x,a>: r ==> P        |] ==> P"
@@ -119,40 +119,40 @@
 AddIs  [fieldCI];
 AddSEs [fieldE];
 
-qed_goal "field_subset" ZF.thy "field(A*B) <= A Un B"
+qed_goal "field_subset" thy "field(A*B) <= A Un B"
  (fn _ => [ (Blast_tac 1) ]);
 
-qed_goalw "domain_subset_field" ZF.thy [field_def]
+qed_goalw "domain_subset_field" thy [field_def]
     "domain(r) <= field(r)"
  (fn _ => [ (rtac Un_upper1 1) ]);
 
-qed_goalw "range_subset_field" ZF.thy [field_def]
+qed_goalw "range_subset_field" thy [field_def]
     "range(r) <= field(r)"
  (fn _ => [ (rtac Un_upper2 1) ]);
 
-qed_goal "domain_times_range" ZF.thy
+qed_goal "domain_times_range" thy
     "!!A B r. r <= Sigma(A,B) ==> r <= domain(r)*range(r)"
  (fn _ => [ (Blast_tac 1) ]);
 
-qed_goal "field_times_field" ZF.thy
+qed_goal "field_times_field" thy
     "!!A B r. r <= Sigma(A,B) ==> r <= field(r)*field(r)"
  (fn _ => [ (Blast_tac 1) ]);
 
 
 (*** Image of a set under a function/relation ***)
 
-qed_goalw "image_iff" ZF.thy [image_def] "b : r``A <-> (EX x:A. <x,b>:r)"
+qed_goalw "image_iff" thy [image_def] "b : r``A <-> (EX x:A. <x,b>:r)"
  (fn _ => [ (Blast_tac 1) ]);
 
-qed_goal "image_singleton_iff" ZF.thy    "b : r``{a} <-> <a,b>:r"
+qed_goal "image_singleton_iff" thy    "b : r``{a} <-> <a,b>:r"
  (fn _ => [ rtac (image_iff RS iff_trans) 1,
             Blast_tac 1 ]);
 
-qed_goalw "imageI" ZF.thy [image_def]
+qed_goalw "imageI" thy [image_def]
     "!!a b r. [| <a,b>: r;  a:A |] ==> b : r``A"
  (fn _ => [ (Blast_tac 1) ]);
 
-qed_goalw "imageE" ZF.thy [image_def]
+qed_goalw "imageE" thy [image_def]
     "[| b: r``A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P"
  (fn major::prems=>
   [ (rtac (major RS CollectE) 1),
@@ -161,32 +161,32 @@
 AddIs  [imageI];
 AddSEs [imageE];
 
-qed_goal "image_subset" ZF.thy "!!A B r. r <= A*B ==> r``C <= B"
+qed_goal "image_subset" thy "!!A B r. r <= A*B ==> r``C <= B"
  (fn _ => [ (Blast_tac 1) ]);
 
 
 (*** Inverse image of a set under a function/relation ***)
 
-qed_goalw "vimage_iff" ZF.thy [vimage_def,image_def,converse_def]
+qed_goalw "vimage_iff" thy [vimage_def,image_def,converse_def]
     "a : r-``B <-> (EX y:B. <a,y>:r)"
  (fn _ => [ (Blast_tac 1) ]);
 
-qed_goal "vimage_singleton_iff" ZF.thy
+qed_goal "vimage_singleton_iff" thy
     "a : r-``{b} <-> <a,b>:r"
  (fn _ => [ rtac (vimage_iff RS iff_trans) 1,
             Blast_tac 1 ]);
 
-qed_goalw "vimageI" ZF.thy [vimage_def]
+qed_goalw "vimageI" thy [vimage_def]
     "!!A B r. [| <a,b>: r;  b:B |] ==> a : r-``B"
  (fn _ => [ (Blast_tac 1) ]);
 
-qed_goalw "vimageE" ZF.thy [vimage_def]
+qed_goalw "vimageE" thy [vimage_def]
     "[| a: r-``B;  !!x.[| <a,x>: r;  x:B |] ==> P |] ==> P"
  (fn major::prems=>
   [ (rtac (major RS imageE) 1),
     (REPEAT (etac converseD 1 ORELSE ares_tac prems 1)) ]);
 
-qed_goalw "vimage_subset" ZF.thy [vimage_def]
+qed_goalw "vimage_subset" thy [vimage_def]
     "!!A B r. r <= A*B ==> r-``C <= A"
  (fn _ => [ (etac (converse_type RS image_subset) 1) ]);
 
@@ -199,22 +199,22 @@
 val ZF_cs = claset() delrules [equalityI];
 
 (** The Union of a set of relations is a relation -- Lemma for fun_Union **)
-goal ZF.thy "!!S. (ALL x:S. EX A B. x <= A*B) ==>  \
+Goal "(ALL x:S. EX A B. x <= A*B) ==>  \
 \                 Union(S) <= domain(Union(S)) * range(Union(S))";
 by (Blast_tac 1);
 qed "rel_Union";
 
 (** The Union of 2 relations is a relation (Lemma for fun_Un)  **)
-qed_goal "rel_Un" ZF.thy
+qed_goal "rel_Un" thy
     "!!r s. [| r <= A*B;  s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)"
  (fn _ => [ (Blast_tac 1) ]);
 
 
-goal ZF.thy "!!r. [| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)";
+Goal "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)";
 by (Blast_tac 1);
 qed "domain_Diff_eq";
 
-goal ZF.thy "!!r. [| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)";
+Goal "[| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)";
 by (Blast_tac 1);
 qed "range_Diff_eq";
 
diff -r ec84178243ff -r f7a5e06adea1 src/ZF/domrange.thy
--- a/src/ZF/domrange.thy	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/domrange.thy	Mon Aug 17 13:09:08 1998 +0200
@@ -1,4 +1,4 @@
 (*Dummy theory to document dependencies *)
 
-domrange = pair + "subset" 
+domrange = pair + subset
 
diff -r ec84178243ff -r f7a5e06adea1 src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/equalities.ML	Mon Aug 17 13:09:08 1998 +0200
@@ -182,7 +182,11 @@
 by (blast_tac (claset() addSEs [equalityE]) 1);
 qed "Union_disjoint";
 
-goalw ZF.thy [Inter_def] "Inter(0) = 0";
+Goal "Union(A) = 0 <-> (ALL B:A. B=0)";
+by (Blast_tac 1);
+qed "Union_empty_iff";
+
+Goalw [Inter_def] "Inter(0) = 0";
 by (Blast_tac 1);
 qed "Inter_0";
 
@@ -209,7 +213,7 @@
 by (Blast_tac 1);
 qed "Union_eq_UN";
 
-goalw ZF.thy [Inter_def] "Inter(A) = (INT x:A. x)";
+Goalw [Inter_def] "Inter(A) = (INT x:A. x)";
 by (Blast_tac 1);
 qed "Inter_eq_INT";
 
@@ -344,10 +348,10 @@
 by (Blast_tac 1);
 qed "domain_of_prod";
 
-qed_goal "domain_0" ZF.thy "domain(0) = 0"
+qed_goal "domain_0" thy "domain(0) = 0"
  (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "domain_cons" ZF.thy
+qed_goal "domain_cons" thy
     "domain(cons(<a,b>,r)) = cons(a, domain(r))"
  (fn _ => [ Blast_tac 1 ]);
 
@@ -376,10 +380,10 @@
 by (Blast_tac 1);
 qed "range_of_prod";
 
-qed_goal "range_0" ZF.thy "range(0) = 0"
+qed_goal "range_0" thy "range(0) = 0"
  (fn _ => [ Blast_tac 1 ]); 
 
-qed_goal "range_cons" ZF.thy
+qed_goal "range_cons" thy
     "range(cons(<a,b>,r)) = cons(b, range(r))"
  (fn _ => [ Blast_tac 1 ]);
 
@@ -404,13 +408,13 @@
 
 (** Field **)
 
-qed_goal "field_of_prod" ZF.thy "field(A*A) = A"
+qed_goal "field_of_prod" thy "field(A*A) = A"
  (fn _ => [ Blast_tac 1 ]); 
 
-qed_goal "field_0" ZF.thy "field(0) = 0"
+qed_goal "field_0" thy "field(0) = 0"
  (fn _ => [ Blast_tac 1 ]); 
 
-qed_goal "field_cons" ZF.thy
+qed_goal "field_cons" thy
     "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
  (fn _ => [ rtac equalityI 1, ALLGOALS (Blast_tac) ]);
 
@@ -543,7 +547,7 @@
 qed "converse_UN";
 
 (*Unfolding Inter avoids using excluded middle on A=0*)
-goalw ZF.thy [Inter_def] "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))";
+Goalw [Inter_def] "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))";
 by (Blast_tac 1);
 qed "converse_INT";
 
diff -r ec84178243ff -r f7a5e06adea1 src/ZF/ex/PropLog.ML
--- a/src/ZF/ex/PropLog.ML	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/ex/PropLog.ML	Mon Aug 17 13:09:08 1998 +0200
@@ -3,7 +3,7 @@
     Author:     Tobias Nipkow & Lawrence C Paulson
     Copyright   1992  University of Cambridge
 
-For ex/prop-log.thy.  Inductive definition of propositional logic.
+Inductive definition of propositional logic.
 Soundness and completeness w.r.t. truth-tables.
 
 Prove: If H|=p then G|=p where G:Fin(H)
@@ -169,23 +169,20 @@
 qed "Imp_Fls";
 
 (*Typical example of strengthening the induction formula*)
-val [major] = goal PropLog.thy 
-    "p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)";
+Goal "p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)";
 by (rtac (split_if RS iffD2) 1);
-by (rtac (major RS prop.induct) 1);
+by (etac prop.induct 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [thms_I, thms.H])));
 by (safe_tac (claset() addSEs [Fls_Imp RS weaken_left_Un1, 
-                            Fls_Imp RS weaken_left_Un2]));
+			       Fls_Imp RS weaken_left_Un2]));
 by (ALLGOALS (fast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, 
                                      weaken_right, Imp_Fls])));
 qed "hyps_thms_if";
 
 (*Key lemma for completeness; yields a set of assumptions satisfying p*)
-val [premp,sat] = goalw PropLog.thy [logcon_def]
-    "[| p: prop;  0 |= p |] ==> hyps(p,t) |- p";
-by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN
-    rtac (premp RS hyps_thms_if) 2);
-by (Fast_tac 1);
+Goalw [logcon_def] "[| p: prop;  0 |= p |] ==> hyps(p,t) |- p";
+by (dtac hyps_thms_if 1);
+by (Asm_full_simp_tac 1);
 qed "logcon_thms_p";
 
 (*For proving certain theorems in our new propositional logic*)
@@ -194,27 +191,24 @@
           addIs [thms_in_pl, thms.H, thms.H RS thms_MP];
 
 (*The excluded middle in the form of an elimination rule*)
-val prems = goal PropLog.thy
-    "[| p: prop;  q: prop |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q";
+Goal "[| p: prop;  q: prop |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q";
 by (rtac (deduction RS deduction) 1);
 by (rtac (thms.DN RS thms_MP) 1);
-by (ALLGOALS (best_tac (thms_cs addSIs prems)));
+by (ALLGOALS (blast_tac thms_cs));
 qed "thms_excluded_middle";
 
 (*Hard to prove directly because it requires cuts*)
-val prems = goal PropLog.thy
-    "[| cons(p,H) |- q;  cons(p=>Fls,H) |- q;  p: prop |] ==> H |- q";
+Goal "[| cons(p,H) |- q;  cons(p=>Fls,H) |- q;  p: prop |] ==> H |- q";
 by (rtac (thms_excluded_middle RS thms_MP RS thms_MP) 1);
-by (REPEAT (resolve_tac (prems@prop.intrs@[deduction,thms_in_pl]) 1));
+by (REPEAT (ares_tac (prop.intrs@[deduction,thms_in_pl]) 1));
 qed "thms_excluded_middle_rule";
 
 (*** Completeness -- lemmas for reducing the set of assumptions ***)
 
 (*For the case hyps(p,t)-cons(#v,Y) |- p;
   we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
-val [major] = goal PropLog.thy
-    "p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
-by (rtac (major RS prop.induct) 1);
+Goal "p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
+by (etac prop.induct 1);
 by (Simp_tac 1);
 by (asm_simp_tac (simpset() setloop (split_tac [split_if])) 1);
 by (fast_tac (claset() addSEs prop.free_SEs) 1);
@@ -224,9 +218,8 @@
 
 (*For the case hyps(p,t)-cons(#v => Fls,Y) |- p;
   we also have hyps(p,t)-{#v=>Fls} <= hyps(p, cons(v,t)) *)
-val [major] = goal PropLog.thy
-    "p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
-by (rtac (major RS prop.induct) 1);
+Goal "p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
+by (etac prop.induct 1);
 by (Simp_tac 1);
 by (asm_simp_tac (simpset() setloop (split_tac [split_if])) 1);
 by (fast_tac (claset() addSEs prop.free_SEs) 1);
@@ -236,19 +229,18 @@
 
 (** Two lemmas for use with weaken_left **)
 
-goal ZF.thy "B-C <= cons(a, B-cons(a,C))";
+Goal "B-C <= cons(a, B-cons(a,C))";
 by (Fast_tac 1);
 qed "cons_Diff_same";
 
-goal ZF.thy "cons(a, B-{c}) - D <= cons(a, B-cons(c,D))";
+Goal "cons(a, B-{c}) - D <= cons(a, B-cons(c,D))";
 by (Fast_tac 1);
 qed "cons_Diff_subset2";
 
 (*The set hyps(p,t) is finite, and elements have the form #v or #v=>Fls;
  could probably prove the stronger hyps(p,t) : Fin(hyps(p,0) Un hyps(p,nat))*)
-val [major] = goal PropLog.thy
-    "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
-by (rtac (major RS prop.induct) 1);
+Goal "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
+by (etac prop.induct 1);
 by (asm_simp_tac (simpset() addsimps [UN_I]
                   setloop (split_tac [split_if])) 2);
 by (ALLGOALS Asm_simp_tac);
diff -r ec84178243ff -r f7a5e06adea1 src/ZF/ex/misc.ML
--- a/src/ZF/ex/misc.ML	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/ex/misc.ML	Mon Aug 17 13:09:08 1998 +0200
@@ -10,12 +10,12 @@
 writeln"ZF/ex/misc";
 
 (*Nice Blast_tac benchmark.  Proved in 0.3s; old tactics can't manage it!*)
-goal ZF.thy "!!S. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
+Goal "ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
 by (Blast_tac 1);
 result();
 
 (*variant of the benchmark above*)
-goal ZF.thy "!!S. ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
+Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
 by (Blast_tac 1);
 result();
 
diff -r ec84178243ff -r f7a5e06adea1 src/ZF/func.ML
--- a/src/ZF/func.ML	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/func.ML	Mon Aug 17 13:09:08 1998 +0200
@@ -8,32 +8,32 @@
 
 (*** The Pi operator -- dependent function space ***)
 
-goalw ZF.thy [Pi_def]
+Goalw [Pi_def]
     "f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)";
 by (Blast_tac 1);
 qed "Pi_iff";
 
 (*For upward compatibility with the former definition*)
-goalw ZF.thy [Pi_def, function_def]
+Goalw [Pi_def, function_def]
     "f: Pi(A,B) <-> f<=Sigma(A,B) & (ALL x:A. EX! y. <x,y>: f)";
 by (Blast_tac 1);
 qed "Pi_iff_old";
 
-goal ZF.thy "!!f. f: Pi(A,B) ==> function(f)";
+Goal "f: Pi(A,B) ==> function(f)";
 by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1);
 qed "fun_is_function";
 
 (**Two "destruct" rules for Pi **)
 
-val [major] = goalw ZF.thy [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)";  
-by (rtac (major RS CollectD1 RS PowD) 1);
+Goalw [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)";  
+by (Blast_tac 1);
 qed "fun_is_rel";
 
-goal ZF.thy "!!f. [| f: Pi(A,B);  a:A |] ==> EX! y. <a,y>: f";  
+Goal "[| f: Pi(A,B);  a:A |] ==> EX! y. <a,y>: f";  
 by (blast_tac (claset() addSDs [Pi_iff_old RS iffD1]) 1);
 qed "fun_unique_Pair";
 
-val prems = goalw ZF.thy [Pi_def]
+val prems = Goalw [Pi_def]
     "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')";
 by (simp_tac (FOL_ss addsimps prems addcongs [Sigma_cong]) 1);
 qed "Pi_cong";
@@ -43,26 +43,26 @@
   Sigmas and Pis are abbreviated as * or -> *)
 
 (*Weakening one function type to another; see also Pi_type*)
-goalw ZF.thy [Pi_def] "!!f. [| f: A->B;  B<=D |] ==> f: A->D";
+Goalw [Pi_def] "[| f: A->B;  B<=D |] ==> f: A->D";
 by (Best_tac 1);
 qed "fun_weaken_type";
 
 (*Empty function spaces*)
-goalw ZF.thy [Pi_def, function_def] "Pi(0,A) = {0}";
+Goalw [Pi_def, function_def] "Pi(0,A) = {0}";
 by (Blast_tac 1);
 qed "Pi_empty1";
 
-goalw ZF.thy [Pi_def] "!!A a. a:A ==> A->0 = 0";
+Goalw [Pi_def] "a:A ==> A->0 = 0";
 by (Blast_tac 1);
 qed "Pi_empty2";
 
 (*The empty function*)
-goalw ZF.thy [Pi_def, function_def] "0: Pi(0,B)";
+Goalw [Pi_def, function_def] "0: Pi(0,B)";
 by (Blast_tac 1);
 qed "empty_fun";
 
 (*The singleton function*)
-goalw ZF.thy [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
+Goalw [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
 by (Blast_tac 1);
 qed "singleton_fun";
 
@@ -70,58 +70,56 @@
 
 (*** Function Application ***)
 
-goalw ZF.thy [Pi_def, function_def]
-     "!!a b f. [| <a,b>: f;  <a,c>: f;  f: Pi(A,B) |] ==> b=c";
+Goalw [Pi_def, function_def]
+     "[| <a,b>: f;  <a,c>: f;  f: Pi(A,B) |] ==> b=c";
 by (Blast_tac 1);
 qed "apply_equality2";
 
-goalw ZF.thy [apply_def, function_def]
-     "!!a b f. [| <a,b>: f;  function(f) |] ==> f`a = b";
+Goalw [apply_def, function_def]
+     "[| <a,b>: f;  function(f) |] ==> f`a = b";
 by (blast_tac (claset() addIs [the_equality]) 1);
 qed "function_apply_equality";
 
-goalw ZF.thy [Pi_def] "!!a b f. [| <a,b>: f;  f: Pi(A,B) |] ==> f`a = b";
+Goalw [Pi_def] "[| <a,b>: f;  f: Pi(A,B) |] ==> f`a = b";
 by (blast_tac (claset() addIs [function_apply_equality]) 1);
 qed "apply_equality";
 
 (*Applying a function outside its domain yields 0*)
-goalw ZF.thy [apply_def]
-    "!!a. a ~: domain(f) ==> f`a = 0";
+Goalw [apply_def]
+    "a ~: domain(f) ==> f`a = 0";
 by (rtac the_0 1);
 by (Blast_tac 1);
 qed "apply_0";
 
-goal ZF.thy "!!f. [| f: Pi(A,B);  c: f |] ==> EX x:A.  c = <x,f`x>";
+Goal "[| f: Pi(A,B);  c: f |] ==> EX x:A.  c = <x,f`x>";
 by (forward_tac [fun_is_rel] 1);
 by (blast_tac (claset() addDs [apply_equality]) 1);
 qed "Pi_memberD";
 
-goal ZF.thy "!!f. [| f: Pi(A,B);  a:A |] ==> <a,f`a>: f";
+Goal "[| f: Pi(A,B);  a:A |] ==> <a,f`a>: f";
 by (rtac (fun_unique_Pair RS ex1E) 1);
 by (resolve_tac [apply_equality RS ssubst] 3);
 by (REPEAT (assume_tac 1));
 qed "apply_Pair";
 
 (*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*)
-goal ZF.thy "!!f. [| f: Pi(A,B);  a:A |] ==> f`a : B(a)"; 
+Goal "[| f: Pi(A,B);  a:A |] ==> f`a : B(a)"; 
 by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1);
 by (REPEAT (ares_tac [apply_Pair] 1));
 qed "apply_type";
 
 (*This version is acceptable to the simplifier*)
-goal ZF.thy "!!f. [| f: A->B;  a:A |] ==> f`a : B"; 
+Goal "[| f: A->B;  a:A |] ==> f`a : B"; 
 by (REPEAT (ares_tac [apply_type] 1));
 qed "apply_funtype";
 
-val [major] = goal ZF.thy
-    "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b";
-by (cut_facts_tac [major RS fun_is_rel] 1);
-by (blast_tac (claset() addSIs [major RS apply_Pair, 
-			      major RSN (2,apply_equality)]) 1);
+Goal "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b";
+by (forward_tac [fun_is_rel] 1);
+by (blast_tac (claset() addSIs [apply_Pair, apply_equality]) 1);
 qed "apply_iff";
 
 (*Refining one Pi type to another*)
-val pi_prem::prems = goal ZF.thy
+val pi_prem::prems = Goal
     "[| f: Pi(A,C);  !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)";
 by (cut_facts_tac [pi_prem] 1);
 by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1);
@@ -131,16 +129,16 @@
 
 (** Elimination of membership in a function **)
 
-goal ZF.thy "!!a A. [| <a,b> : f;  f: Pi(A,B) |] ==> a : A";
+Goal "[| <a,b> : f;  f: Pi(A,B) |] ==> a : A";
 by (REPEAT (ares_tac [fun_is_rel RS subsetD RS SigmaD1] 1));
 qed "domain_type";
 
-goal ZF.thy "!!b B a. [| <a,b> : f;  f: Pi(A,B) |] ==> b : B(a)";
+Goal "[| <a,b> : f;  f: Pi(A,B) |] ==> b : B(a)";
 by (etac (fun_is_rel RS subsetD RS SigmaD2) 1);
 by (assume_tac 1);
 qed "range_type";
 
-val prems = goal ZF.thy
+val prems = Goal
     "[| <a,b>: f;  f: Pi(A,B);       \
 \       [| a:A;  b:B(a);  f`a = b |] ==> P  \
 \    |] ==> P";
@@ -151,35 +149,35 @@
 
 (*** Lambda Abstraction ***)
 
-goalw ZF.thy [lam_def] "!!A b. a:A ==> <a,b(a)> : (lam x:A. b(x))";  
+Goalw [lam_def] "a:A ==> <a,b(a)> : (lam x:A. b(x))";  
 by (etac RepFunI 1);
 qed "lamI";
 
-val major::prems = goalw ZF.thy [lam_def]
+val major::prems = Goalw [lam_def]
     "[| p: (lam x:A. b(x));  !!x.[| x:A; p=<x,b(x)> |] ==> P  \
 \    |] ==>  P";  
 by (rtac (major RS RepFunE) 1);
 by (REPEAT (ares_tac prems 1));
 qed "lamE";
 
-goal ZF.thy "!!a b c. [| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)";  
+Goal "[| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)";  
 by (REPEAT (eresolve_tac [asm_rl,lamE,Pair_inject,ssubst] 1));
 qed "lamD";
 
-val prems = goalw ZF.thy [lam_def, Pi_def, function_def]
+val prems = Goalw [lam_def, Pi_def, function_def]
     "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)";  
 by (blast_tac (claset() addIs prems) 1);
 qed "lam_type";
 
-goal ZF.thy "(lam x:A. b(x)) : A -> {b(x). x:A}";
+Goal "(lam x:A. b(x)) : A -> {b(x). x:A}";
 by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1));
 qed "lam_funtype";
 
-goal ZF.thy "!!a A. a : A ==> (lam x:A. b(x)) ` a = b(a)";
+Goal "a : A ==> (lam x:A. b(x)) ` a = b(a)";
 by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1));
 qed "beta";
 
-goalw ZF.thy [lam_def] "(lam x:0. b(x)) = 0";
+Goalw [lam_def] "(lam x:0. b(x)) = 0";
 by (Simp_tac 1);
 qed "lam_empty";
 
@@ -190,14 +188,14 @@
 Addsimps [beta, lam_empty, domain_lam];
 
 (*congruence rule for lambda abstraction*)
-val prems = goalw ZF.thy [lam_def] 
+val prems = Goalw [lam_def] 
     "[| A=A';  !!x. x:A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')";
 by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1);
 qed "lam_cong";
 
 Addcongs [lam_cong];
 
-val [major] = goal ZF.thy
+val [major] = Goal
     "(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)";
 by (res_inst_tac [("x", "lam x: A. THE y. Q(x,y)")] exI 1);
 by (rtac ballI 1);
@@ -210,7 +208,7 @@
 (** Extensionality **)
 
 (*Semi-extensionality!*)
-val prems = goal ZF.thy
+val prems = Goal
     "[| f : Pi(A,B);  g: Pi(C,D);  A<=C; \
 \       !!x. x:A ==> f`x = g`x       |] ==> f<=g";
 by (rtac subsetI 1);
@@ -220,27 +218,27 @@
 by (REPEAT (ares_tac (prems@[apply_Pair,subsetD]) 1));
 qed "fun_subset";
 
-val prems = goal ZF.thy
+val prems = Goal
     "[| f : Pi(A,B);  g: Pi(A,D);  \
 \       !!x. x:A ==> f`x = g`x       |] ==> f=g";
 by (REPEAT (ares_tac (prems @ (prems RL [sym]) @
                       [subset_refl,equalityI,fun_subset]) 1));
 qed "fun_extension";
 
-goal ZF.thy "!!f A B. f : Pi(A,B) ==> (lam x:A. f`x) = f";
+Goal "f : Pi(A,B) ==> (lam x:A. f`x) = f";
 by (rtac fun_extension 1);
 by (REPEAT (ares_tac [lam_type,apply_type,beta] 1));
 qed "eta";
 
 Addsimps [eta];
 
-val fun_extension_iff = prove_goal ZF.thy
-  "!!z. [| f:Pi(A,B); g:Pi(A,C) |] ==> (ALL a:A. f`a = g`a) <-> f=g"
- (fn _=> [ (blast_tac (claset() addIs [fun_extension]) 1) ]);
+Goal "[| f:Pi(A,B); g:Pi(A,C) |] ==> (ALL a:A. f`a = g`a) <-> f=g";
+by (blast_tac (claset() addIs [fun_extension]) 1);
+qed "fun_extension_iff";
 
 (*thanks to Mark Staples*)
-val fun_subset_eq = prove_goal ZF.thy
-    "!!z. [| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)"
+val fun_subset_eq = prove_goal thy
+    "!!f. [| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)"
  (fn _=> 
   [ (rtac iffI 1), (asm_full_simp_tac ZF_ss 2),
     (rtac fun_extension 1), (REPEAT (atac 1)),
@@ -249,7 +247,7 @@
 
 
 (*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
-val prems = goal ZF.thy
+val prems = Goal
     "[| f: Pi(A,B);        \
 \       !!b. [| ALL x:A. b(x):B(x);  f = (lam x:A. b(x)) |] ==> P   \
 \    |] ==> P";
@@ -261,14 +259,13 @@
 
 (** Images of functions **)
 
-goalw ZF.thy [lam_def] "!!C A. C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}";
+Goalw [lam_def] "C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}";
 by (Blast_tac 1);
 qed "image_lam";
 
-goal ZF.thy "!!C A. [| f : Pi(A,B);  C <= A |] ==> f``C = {f`x. x:C}";
+Goal "[| f : Pi(A,B);  C <= A |] ==> f``C = {f`x. x:C}";
 by (etac (eta RS subst) 1);
-by (asm_full_simp_tac (FOL_ss addsimps [beta, image_lam, subset_iff]
-                              addcongs [RepFun_cong]) 1);
+by (asm_full_simp_tac (simpset() addsimps [image_lam, subset_iff]) 1);
 qed "image_fun";
 
 Goal "[| f: Pi(A,B);  x: A |] ==> f `` cons(x,y) = cons(f`x, f``y)";
@@ -278,47 +275,46 @@
 
 (*** properties of "restrict" ***)
 
-goalw ZF.thy [restrict_def,lam_def]
-    "!!f A. [| f: Pi(C,B);  A<=C |] ==> restrict(f,A) <= f";
+Goalw [restrict_def,lam_def]
+    "[| f: Pi(C,B);  A<=C |] ==> restrict(f,A) <= f";
 by (blast_tac (claset() addIs [apply_Pair]) 1);
 qed "restrict_subset";
 
-val prems = goalw ZF.thy [restrict_def]
+val prems = Goalw [restrict_def]
     "[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)";  
 by (rtac lam_type 1);
 by (eresolve_tac prems 1);
 qed "restrict_type";
 
-val [pi,subs] = goal ZF.thy 
-    "[| f: Pi(C,B);  A<=C |] ==> restrict(f,A) : Pi(A,B)";  
-by (rtac (pi RS apply_type RS restrict_type) 1);
-by (etac (subs RS subsetD) 1);
+Goal "[| f: Pi(C,B);  A<=C |] ==> restrict(f,A) : Pi(A,B)";  
+by (blast_tac (claset() addIs [apply_type, restrict_type]) 1);
 qed "restrict_type2";
 
-goalw ZF.thy [restrict_def] "!!a A. a : A ==> restrict(f,A) ` a = f`a";
+Goalw [restrict_def] "a : A ==> restrict(f,A) ` a = f`a";
 by (etac beta 1);
 qed "restrict";
 
-goalw ZF.thy [restrict_def] "restrict(f,0) = 0";
+Goalw [restrict_def] "restrict(f,0) = 0";
 by (Simp_tac 1);
 qed "restrict_empty";
 
 Addsimps [restrict, restrict_empty];
 
 (*NOT SAFE as a congruence rule for the simplifier!  Can cause it to fail!*)
-val prems = goalw ZF.thy [restrict_def]
+val prems = Goalw [restrict_def]
     "[| A=B;  !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)";
 by (REPEAT (ares_tac (prems@[lam_cong]) 1));
 qed "restrict_eqI";
 
-goalw ZF.thy [restrict_def, lam_def] "domain(restrict(f,C)) = C";
+Goalw [restrict_def, lam_def] "domain(restrict(f,C)) = C";
 by (Blast_tac 1);
 qed "domain_restrict";
 
-val [prem] = goalw ZF.thy [restrict_def]
+Goalw [restrict_def]
     "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";
 by (rtac (refl RS lam_cong) 1);
-by (etac (prem RS subsetD RS beta) 1);  (*easier than calling simp_tac*)
+by (set_mp_tac 1);
+by (Asm_simp_tac 1);
 qed "restrict_lam_eq";
 
 
@@ -327,16 +323,16 @@
 
 (** The Union of a set of COMPATIBLE functions is a function **)
 
-goalw ZF.thy [function_def]
-    "!!S. [| ALL x:S. function(x); \
+Goalw [function_def]
+    "[| ALL x:S. function(x); \
 \            ALL x:S. ALL y:S. x<=y | y<=x  |] ==>  \
 \         function(Union(S))";
 by (fast_tac (ZF_cs addSDs [bspec RS bspec]) 1);
 	(*by (Blast_tac 1);  takes too long...*)
 qed "function_Union";
 
-goalw ZF.thy [Pi_def]
-    "!!S. [| ALL f:S. EX C D. f:C->D; \
+Goalw [Pi_def]
+    "[| ALL f:S. EX C D. f:C->D; \
 \            ALL f:S. ALL y:S. f<=y | y<=f  |] ==>  \
 \         Union(S) : domain(Union(S)) -> range(Union(S))";
 by (blast_tac (subset_cs addSIs [rel_Union, function_Union]) 1);
@@ -349,7 +345,7 @@
               Un_upper1 RSN (2, subset_trans), 
               Un_upper2 RSN (2, subset_trans)];
 
-goal ZF.thy "!!f. [| f: A->B;  g: C->D;  A Int C = 0  |]  \
+Goal "[| f: A->B;  g: C->D;  A Int C = 0  |]  \
 \                 ==> (f Un g) : (A Un C) -> (B Un D)";
 (*Prove the product and domain subgoals using distributive laws*)
 by (asm_full_simp_tac (simpset() addsimps [Pi_iff,extension]@Un_rls) 1);
@@ -357,15 +353,13 @@
 by (Blast_tac 1);
 qed "fun_disjoint_Un";
 
-goal ZF.thy
-    "!!f g a. [| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
+Goal "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
 \             (f Un g)`a = f`a";
 by (rtac (apply_Pair RS UnI1 RS apply_equality) 1);
 by (REPEAT (ares_tac [fun_disjoint_Un] 1));
 qed "fun_disjoint_apply1";
 
-goal ZF.thy
-    "!!f g c. [| c:C;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
+Goal "[| c:C;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
 \             (f Un g)`c = g`c";
 by (rtac (apply_Pair RS UnI2 RS apply_equality) 1);
 by (REPEAT (ares_tac [fun_disjoint_Un] 1));
@@ -373,18 +367,17 @@
 
 (** Domain and range of a function/relation **)
 
-goalw ZF.thy [Pi_def] "!!f. f : Pi(A,B) ==> domain(f)=A";
+Goalw [Pi_def] "f : Pi(A,B) ==> domain(f)=A";
 by (Blast_tac 1);
 qed "domain_of_fun";
 
-goal ZF.thy "!!f. [| f : Pi(A,B);  a: A |] ==> f`a : range(f)";
+Goal "[| f : Pi(A,B);  a: A |] ==> f`a : range(f)";
 by (etac (apply_Pair RS rangeI) 1);
 by (assume_tac 1);
 qed "apply_rangeI";
 
-val [major] = goal ZF.thy "f : Pi(A,B) ==> f : A->range(f)";
-by (rtac (major RS Pi_type) 1);
-by (etac (major RS apply_rangeI) 1);
+Goal "f : Pi(A,B) ==> f : A->range(f)";
+by (REPEAT (ares_tac [Pi_type, apply_rangeI] 1));
 qed "range_of_fun";
 
 (*** Extensions of functions ***)
diff -r ec84178243ff -r f7a5e06adea1 src/ZF/mono.ML
--- a/src/ZF/mono.ML	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/mono.ML	Mon Aug 17 13:09:08 1998 +0200
@@ -28,7 +28,7 @@
 by (Blast_tac 1);
 qed "Union_mono";
 
-val prems = goal thy
+val prems = Goal
     "[| A<=C;  !!x. x:A ==> B(x)<=D(x) \
 \    |] ==> (UN x:A. B(x)) <= (UN x:C. D(x))";
 by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
@@ -57,8 +57,7 @@
 
 (** Standard products, sums and function spaces **)
 
-Goal "[| A<=C;  ALL x:A. B(x) <= D(x) |] ==> \
-\                       Sigma(A,B) <= Sigma(C,D)";
+Goal "[| A<=C;  ALL x:A. B(x) <= D(x) |] ==> Sigma(A,B) <= Sigma(C,D)";
 by (Blast_tac 1);
 qed "Sigma_mono_lemma";
 val Sigma_mono = ballI RSN (2,Sigma_mono_lemma);
@@ -131,12 +130,12 @@
 
 (** Images **)
 
-val [prem1,prem2] = goal thy
+val [prem1,prem2] = Goal
     "[| !! x y. <x,y>:r ==> <x,y>:s;  A<=B |] ==> r``A <= s``B";
 by (blast_tac (claset() addIs [prem1, prem2 RS subsetD]) 1);
 qed "image_pair_mono";
 
-val [prem1,prem2] = goal thy
+val [prem1,prem2] = Goal
     "[| !! x y. <x,y>:r ==> <x,y>:s;  A<=B |] ==> r-``A <= s-``B";
 by (blast_tac (claset() addIs [prem1, prem2 RS subsetD]) 1);
 qed "vimage_pair_mono";
@@ -149,7 +148,7 @@
 by (Blast_tac 1);
 qed "vimage_mono";
 
-val [sub,PQimp] = goal thy
+val [sub,PQimp] = Goal
     "[| A<=B;  !!x. x:A ==> P(x) --> Q(x) |] ==> Collect(A,P) <= Collect(B,Q)";
 by (blast_tac (claset() addIs [sub RS subsetD, PQimp RS mp]) 1);
 qed "Collect_mono";
diff -r ec84178243ff -r f7a5e06adea1 src/ZF/mono.thy
--- a/src/ZF/mono.thy	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/mono.thy	Mon Aug 17 13:09:08 1998 +0200
@@ -1,4 +1,2 @@
-(*Dummy theory to document dependencies *)
+mono = QPair + Sum + func
 
-mono = QPair + Sum + domrange
-
diff -r ec84178243ff -r f7a5e06adea1 src/ZF/pair.ML
--- a/src/ZF/pair.ML	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/pair.ML	Mon Aug 17 13:09:08 1998 +0200
@@ -8,17 +8,17 @@
 
 (** Lemmas for showing that <a,b> uniquely determines a and b **)
 
-qed_goal "singleton_eq_iff" ZF.thy
+qed_goal "singleton_eq_iff" thy
     "{a} = {b} <-> a=b"
  (fn _=> [ (resolve_tac [extension RS iff_trans] 1),
            (Blast_tac 1) ]);
 
-qed_goal "doubleton_eq_iff" ZF.thy
+qed_goal "doubleton_eq_iff" thy
     "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"
  (fn _=> [ (resolve_tac [extension RS iff_trans] 1),
            (Blast_tac 1) ]);
 
-qed_goalw "Pair_iff" ZF.thy [Pair_def]
+qed_goalw "Pair_iff" thy [Pair_def]
     "<a,b> = <c,d> <-> a=c & b=d"
  (fn _=> [ (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1),
            (Blast_tac 1) ]);
@@ -32,20 +32,20 @@
 bind_thm ("Pair_inject1", Pair_iff RS iffD1 RS conjunct1);
 bind_thm ("Pair_inject2", Pair_iff RS iffD1 RS conjunct2);
 
-qed_goalw "Pair_not_0" ZF.thy [Pair_def] "<a,b> ~= 0"
+qed_goalw "Pair_not_0" thy [Pair_def] "<a,b> ~= 0"
  (fn _ => [ (blast_tac (claset() addEs [equalityE]) 1) ]);
 
 bind_thm ("Pair_neq_0", Pair_not_0 RS notE);
 
 AddSEs [Pair_neq_0, sym RS Pair_neq_0];
 
-qed_goalw "Pair_neq_fst" ZF.thy [Pair_def] "<a,b>=a ==> P"
+qed_goalw "Pair_neq_fst" thy [Pair_def] "<a,b>=a ==> P"
  (fn [major]=>
   [ (rtac (consI1 RS mem_asym RS FalseE) 1),
     (rtac (major RS subst) 1),
     (rtac consI1 1) ]);
 
-qed_goalw "Pair_neq_snd" ZF.thy [Pair_def] "<a,b>=b ==> P"
+qed_goalw "Pair_neq_snd" thy [Pair_def] "<a,b>=b ==> P"
  (fn [major]=>
   [ (rtac (consI1 RS consI2 RS mem_asym RS FalseE) 1),
     (rtac (major RS subst) 1),
@@ -55,12 +55,12 @@
 (*** Sigma: Disjoint union of a family of sets
      Generalizes Cartesian product ***)
 
-qed_goalw "Sigma_iff" ZF.thy [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
+qed_goalw "Sigma_iff" thy [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
  (fn _ => [ Blast_tac 1 ]);
 
 Addsimps [Sigma_iff];
 
-qed_goal "SigmaI" ZF.thy
+qed_goal "SigmaI" thy
     "!!a b. [| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)"
  (fn _ => [ Asm_simp_tac 1 ]);
 
@@ -68,7 +68,7 @@
 bind_thm ("SigmaD2", Sigma_iff RS iffD1 RS conjunct2);
 
 (*The general elimination rule*)
-qed_goalw "SigmaE" ZF.thy [Sigma_def]
+qed_goalw "SigmaE" thy [Sigma_def]
     "[| c: Sigma(A,B);  \
 \       !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P \
 \    |] ==> P"
@@ -76,7 +76,7 @@
   [ (cut_facts_tac [major] 1),
     (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
 
-qed_goal "SigmaE2" ZF.thy
+qed_goal "SigmaE2" thy
     "[| <a,b> : Sigma(A,B);    \
 \       [| a:A;  b:B(a) |] ==> P   \
 \    |] ==> P"
@@ -85,7 +85,7 @@
     (rtac (major RS SigmaD1) 1),
     (rtac (major RS SigmaD2) 1) ]);
 
-qed_goalw "Sigma_cong" ZF.thy [Sigma_def]
+qed_goalw "Sigma_cong" thy [Sigma_def]
     "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
 \    Sigma(A,B) = Sigma(A',B')"
  (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
@@ -98,10 +98,10 @@
 AddSIs [SigmaI];
 AddSEs [SigmaE2, SigmaE];
 
-qed_goal "Sigma_empty1" ZF.thy "Sigma(0,B) = 0"
+qed_goal "Sigma_empty1" thy "Sigma(0,B) = 0"
  (fn _ => [ (Blast_tac 1) ]);
 
-qed_goal "Sigma_empty2" ZF.thy "A*0 = 0"
+qed_goal "Sigma_empty2" thy "A*0 = 0"
  (fn _ => [ (Blast_tac 1) ]);
 
 Addsimps [Sigma_empty1, Sigma_empty2];
@@ -113,21 +113,21 @@
 
 (*** Projections: fst, snd ***)
 
-qed_goalw "fst_conv" ZF.thy [fst_def] "fst(<a,b>) = a"
+qed_goalw "fst_conv" thy [fst_def] "fst(<a,b>) = a"
  (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]);
 
-qed_goalw "snd_conv" ZF.thy [snd_def] "snd(<a,b>) = b"
+qed_goalw "snd_conv" thy [snd_def] "snd(<a,b>) = b"
  (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]);
 
 Addsimps [fst_conv,snd_conv];
 
-qed_goal "fst_type" ZF.thy "!!p. p:Sigma(A,B) ==> fst(p) : A"
+qed_goal "fst_type" thy "!!p. p:Sigma(A,B) ==> fst(p) : A"
  (fn _=> [ Auto_tac ]);
 
-qed_goal "snd_type" ZF.thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))"
+qed_goal "snd_type" thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))"
  (fn _=> [ Auto_tac ]);
 
-qed_goal "Pair_fst_snd_eq" ZF.thy
+qed_goal "Pair_fst_snd_eq" thy
     "!!a A B. a: Sigma(A,B) ==> <fst(a),snd(a)> = a"
  (fn _=> [ Auto_tac ]);
 
@@ -135,13 +135,13 @@
 (*** Eliminator - split ***)
 
 (*A META-equality, so that it applies to higher types as well...*)
-qed_goalw "split" ZF.thy [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)"
+qed_goalw "split" thy [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)"
  (fn _ => [ (Simp_tac 1),
             (rtac reflexive_thm 1) ]);
 
 Addsimps [split];
 
-qed_goal "split_type" ZF.thy
+qed_goal "split_type" thy
     "[|  p:Sigma(A,B);   \
 \        !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \
 \    |] ==> split(%x y. c(x,y), p) : C(p)"
@@ -149,8 +149,8 @@
   [ (rtac (major RS SigmaE) 1),
     (asm_simp_tac (simpset() addsimps prems) 1) ]);
 
-goalw ZF.thy [split_def]
-  "!!u. u: A*B ==>   \
+Goalw [split_def]
+  "u: A*B ==>   \
 \       R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))";
 by Auto_tac;
 qed "expand_split";
@@ -158,11 +158,11 @@
 
 (*** split for predicates: result type o ***)
 
-goalw ZF.thy [split_def] "!!R a b. R(a,b) ==> split(R, <a,b>)";
+Goalw [split_def] "R(a,b) ==> split(R, <a,b>)";
 by (Asm_simp_tac 1);
 qed "splitI";
 
-val major::sigma::prems = goalw ZF.thy [split_def]
+val major::sigma::prems = Goalw [split_def]
     "[| split(R,z);  z:Sigma(A,B);                      \
 \       !!x y. [| z = <x,y>;  R(x,y) |] ==> P           \
 \    |] ==> P";
@@ -172,7 +172,7 @@
 by (Asm_full_simp_tac 1);
 qed "splitE";
 
-goalw ZF.thy [split_def] "!!R a b. split(R,<a,b>) ==> R(a,b)";
+Goalw [split_def] "split(R,<a,b>) ==> R(a,b)";
 by (Full_simp_tac 1);
 qed "splitD";
 
diff -r ec84178243ff -r f7a5e06adea1 src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/simpdata.ML	Mon Aug 17 13:09:08 1998 +0200
@@ -10,7 +10,7 @@
 
 local
   (*For proving rewrite rules*)
-  fun prover s = (prove_goal ZF.thy s (fn _ => [Blast_tac 1]));
+  fun prover s = (prove_goal thy s (fn _ => [Blast_tac 1]));
 
 in
 
diff -r ec84178243ff -r f7a5e06adea1 src/ZF/subset.ML
--- a/src/ZF/subset.ML	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/subset.ML	Mon Aug 17 13:09:08 1998 +0200
@@ -9,38 +9,38 @@
 
 (*** cons ***)
 
-qed_goal "cons_subsetI" ZF.thy "!!a. [| a:C; B<=C |] ==> cons(a,B) <= C"
+qed_goal "cons_subsetI" thy "!!a. [| a:C; B<=C |] ==> cons(a,B) <= C"
  (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "subset_consI" ZF.thy "B <= cons(a,B)"
+qed_goal "subset_consI" thy "B <= cons(a,B)"
  (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "cons_subset_iff" ZF.thy "cons(a,B)<=C <-> a:C & B<=C"
+qed_goal "cons_subset_iff" thy "cons(a,B)<=C <-> a:C & B<=C"
  (fn _ => [ Blast_tac 1 ]);
 
 (*A safe special case of subset elimination, adding no new variables 
   [| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *)
 bind_thm ("cons_subsetE", cons_subset_iff RS iffD1 RS conjE);
 
-qed_goal "subset_empty_iff" ZF.thy "A<=0 <-> A=0"
+qed_goal "subset_empty_iff" thy "A<=0 <-> A=0"
  (fn _=> [ (Blast_tac 1) ]);
 
-qed_goal "subset_cons_iff" ZF.thy
+qed_goal "subset_cons_iff" thy
     "C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)"
  (fn _=> [ (Blast_tac 1) ]);
 
 (*** succ ***)
 
-qed_goal "subset_succI" ZF.thy "i <= succ(i)"
+qed_goal "subset_succI" thy "i <= succ(i)"
  (fn _=> [ (Blast_tac 1) ]);
 
 (*But if j is an ordinal or is transitive, then i:j implies i<=j! 
   See ordinal/Ord_succ_subsetI*)
-qed_goalw "succ_subsetI" ZF.thy [succ_def]
+qed_goalw "succ_subsetI" thy [succ_def]
     "!!i j. [| i:j;  i<=j |] ==> succ(i)<=j"
  (fn _=> [ (Blast_tac 1) ]);
 
-qed_goalw "succ_subsetE" ZF.thy [succ_def] 
+qed_goalw "succ_subsetE" thy [succ_def] 
     "[| succ(i) <= j;  [| i:j;  i<=j |] ==> P \
 \    |] ==> P"
  (fn major::prems=>
@@ -49,22 +49,22 @@
 
 (*** singletons ***)
 
-qed_goal "singleton_subsetI" ZF.thy "!!a c. a:C ==> {a} <= C"
+qed_goal "singleton_subsetI" thy "!!a c. a:C ==> {a} <= C"
  (fn _=> [ (Blast_tac 1) ]);
 
-qed_goal "singleton_subsetD" ZF.thy "!!a C. {a} <= C  ==>  a:C"
+qed_goal "singleton_subsetD" thy "!!a C. {a} <= C  ==>  a:C"
  (fn _=> [ (Blast_tac 1) ]);
 
 (*** Big Union -- least upper bound of a set  ***)
 
-qed_goal "Union_subset_iff" ZF.thy "Union(A) <= C <-> (ALL x:A. x <= C)"
+qed_goal "Union_subset_iff" thy "Union(A) <= C <-> (ALL x:A. x <= C)"
  (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Union_upper" ZF.thy
+qed_goal "Union_upper" thy
     "!!B A. B:A ==> B <= Union(A)"
  (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Union_least" ZF.thy
+qed_goal "Union_least" thy
     "[| !!x. x:A ==> x<=C |] ==> Union(A) <= C"
  (fn [prem]=>
   [ (rtac (ballI RS (Union_subset_iff RS iffD2)) 1),
@@ -72,19 +72,19 @@
 
 (*** Union of a family of sets  ***)
 
-goal ZF.thy "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))";
+Goal "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))";
 by (blast_tac (claset() addSEs [equalityE]) 1);
 qed "subset_UN_iff_eq";
 
-qed_goal "UN_subset_iff" ZF.thy
+qed_goal "UN_subset_iff" thy
      "(UN x:A. B(x)) <= C <-> (ALL x:A. B(x) <= C)"
  (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "UN_upper" ZF.thy
+qed_goal "UN_upper" thy
     "!!x A. x:A ==> B(x) <= (UN x:A. B(x))"
  (fn _ => [ etac (RepFunI RS Union_upper) 1 ]);
 
-qed_goal "UN_least" ZF.thy
+qed_goal "UN_least" thy
     "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C"
  (fn [prem]=>
   [ (rtac (ballI RS (UN_subset_iff RS iffD2)) 1),
@@ -93,14 +93,14 @@
 
 (*** Big Intersection -- greatest lower bound of a nonempty set ***)
 
-qed_goal "Inter_subset_iff" ZF.thy
+qed_goal "Inter_subset_iff" thy
      "!!a A. a: A  ==>  C <= Inter(A) <-> (ALL x:A. C <= x)"
  (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Inter_lower" ZF.thy "!!B A. B:A ==> Inter(A) <= B"
+qed_goal "Inter_lower" thy "!!B A. B:A ==> Inter(A) <= B"
  (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Inter_greatest" ZF.thy
+qed_goal "Inter_greatest" thy
     "[| a:A;  !!x. x:A ==> C<=x |] ==> C <= Inter(A)"
  (fn [prem1,prem2]=>
   [ (rtac ([prem1, ballI] MRS (Inter_subset_iff RS iffD2)) 1),
@@ -108,11 +108,11 @@
 
 (*** Intersection of a family of sets  ***)
 
-qed_goal "INT_lower" ZF.thy
+qed_goal "INT_lower" thy
     "!!x. x:A ==> (INT x:A. B(x)) <= B(x)"
  (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "INT_greatest" ZF.thy
+qed_goal "INT_greatest" thy
     "[| a:A;  !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))"
  (fn [nonempty,prem] =>
   [ rtac (nonempty RS RepFunI RS Inter_greatest) 1,
@@ -121,53 +121,58 @@
 
 (*** Finite Union -- the least upper bound of 2 sets ***)
 
-qed_goal "Un_subset_iff" ZF.thy "A Un B <= C <-> A <= C & B <= C"
+qed_goal "Un_subset_iff" thy "A Un B <= C <-> A <= C & B <= C"
  (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Un_upper1" ZF.thy "A <= A Un B"
+qed_goal "Un_upper1" thy "A <= A Un B"
  (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Un_upper2" ZF.thy "B <= A Un B"
+qed_goal "Un_upper2" thy "B <= A Un B"
  (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Un_least" ZF.thy "!!A B C. [| A<=C;  B<=C |] ==> A Un B <= C"
+qed_goal "Un_least" thy "!!A B C. [| A<=C;  B<=C |] ==> A Un B <= C"
  (fn _ => [ Blast_tac 1 ]);
 
 
 (*** Finite Intersection -- the greatest lower bound of 2 sets *)
 
-qed_goal "Int_subset_iff" ZF.thy "C <= A Int B <-> C <= A & C <= B"
+qed_goal "Int_subset_iff" thy "C <= A Int B <-> C <= A & C <= B"
  (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Int_lower1" ZF.thy "A Int B <= A"
+qed_goal "Int_lower1" thy "A Int B <= A"
  (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Int_lower2" ZF.thy "A Int B <= B"
+qed_goal "Int_lower2" thy "A Int B <= B"
  (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Int_greatest" ZF.thy "!!A B C. [| C<=A;  C<=B |] ==> C <= A Int B"
+qed_goal "Int_greatest" thy "!!A B C. [| C<=A;  C<=B |] ==> C <= A Int B"
  (fn _ => [ Blast_tac 1 ]);
 
 
 (*** Set difference *)
 
-qed_goal "Diff_subset" ZF.thy "A-B <= A"
+qed_goal "Diff_subset" thy "A-B <= A"
  (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Diff_contains" ZF.thy
+qed_goal "Diff_contains" thy
     "!!C. [| C<=A;  C Int B = 0 |] ==> C <= A-B"
- (fn _ => [ (blast_tac (claset() addSEs [equalityE]) 1) ]);
+ (fn _ => [ Blast_tac 1 ]);
+
+Goal "B <= A - cons(c,C)  <->  B<=A-C & c ~: B";
+by (Blast_tac 1);
+qed "subset_Diff_cons_iff";
+
 
 
 (** Collect **)
 
-qed_goal "Collect_subset" ZF.thy "Collect(A,P) <= A"
+qed_goal "Collect_subset" thy "Collect(A,P) <= A"
  (fn _ => [ Blast_tac 1 ]);
 
 
 (** RepFun **)
 
-val prems = goal ZF.thy "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B";
+val prems = Goal "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B";
 by (blast_tac (claset() addIs prems) 1);
 qed "RepFun_subset";
 
diff -r ec84178243ff -r f7a5e06adea1 src/ZF/upair.ML
--- a/src/ZF/upair.ML	Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/upair.ML	Mon Aug 17 13:09:08 1998 +0200
@@ -21,19 +21,19 @@
 
 (*** Unordered pairs - Upair ***)
 
-qed_goalw "Upair_iff" ZF.thy [Upair_def]
+qed_goalw "Upair_iff" thy [Upair_def]
     "c : Upair(a,b) <-> (c=a | c=b)"
  (fn _ => [ (blast_tac (claset() addEs [Pow_neq_0, sym RS Pow_neq_0]) 1) ]);
 
 Addsimps [Upair_iff];
 
-qed_goal "UpairI1" ZF.thy "a : Upair(a,b)"
+qed_goal "UpairI1" thy "a : Upair(a,b)"
  (fn _ => [ Simp_tac 1 ]);
 
-qed_goal "UpairI2" ZF.thy "b : Upair(a,b)"
+qed_goal "UpairI2" thy "b : Upair(a,b)"
  (fn _ => [ Simp_tac 1 ]);
 
-qed_goal "UpairE" ZF.thy
+qed_goal "UpairE" thy
     "[| a : Upair(b,c);  a=b ==> P;  a=c ==> P |] ==> P"
  (fn major::prems=>
   [ (rtac (major RS (Upair_iff RS iffD1 RS disjE)) 1),
@@ -44,25 +44,25 @@
 
 (*** Rules for binary union -- Un -- defined via Upair ***)
 
-qed_goalw "Un_iff" ZF.thy [Un_def] "c : A Un B <-> (c:A | c:B)"
+qed_goalw "Un_iff" thy [Un_def] "c : A Un B <-> (c:A | c:B)"
  (fn _ => [ Blast_tac 1 ]);
 
 Addsimps [Un_iff];
 
-qed_goal "UnI1" ZF.thy "!!c. c : A ==> c : A Un B"
+qed_goal "UnI1" thy "!!c. c : A ==> c : A Un B"
  (fn _ => [ Asm_simp_tac 1 ]);
 
-qed_goal "UnI2" ZF.thy "!!c. c : B ==> c : A Un B"
+qed_goal "UnI2" thy "!!c. c : B ==> c : A Un B"
  (fn _ => [ Asm_simp_tac 1 ]);
 
-qed_goal "UnE" ZF.thy 
+qed_goal "UnE" thy 
     "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P"
  (fn major::prems=>
   [ (rtac (major RS (Un_iff RS iffD1 RS disjE)) 1),
     (REPEAT (eresolve_tac prems 1)) ]);
 
 (*Stronger version of the rule above*)
-qed_goal "UnE'" ZF.thy
+qed_goal "UnE'" thy
     "[| c : A Un B;  c:A ==> P;  [| c:B;  c~:A |] ==> P |] ==> P"
  (fn major::prems =>
   [(rtac (major RS UnE) 1),
@@ -73,7 +73,7 @@
    (etac notnotD 1)]);
 
 (*Classical introduction rule: no commitment to A vs B*)
-qed_goal "UnCI" ZF.thy "(c ~: B ==> c : A) ==> c : A Un B"
+qed_goal "UnCI" thy "(c ~: B ==> c : A) ==> c : A Un B"
  (fn prems=>
   [ Simp_tac 1, blast_tac (claset() addSIs prems) 1 ]);
 
@@ -83,21 +83,21 @@
 
 (*** Rules for small intersection -- Int -- defined via Upair ***)
 
-qed_goalw "Int_iff" ZF.thy [Int_def] "c : A Int B <-> (c:A & c:B)"
+qed_goalw "Int_iff" thy [Int_def] "c : A Int B <-> (c:A & c:B)"
  (fn _ => [ Blast_tac 1 ]);
 
 Addsimps [Int_iff];
 
-qed_goal "IntI" ZF.thy "!!c. [| c : A;  c : B |] ==> c : A Int B"
+qed_goal "IntI" thy "!!c. [| c : A;  c : B |] ==> c : A Int B"
  (fn _ => [ Asm_simp_tac 1 ]);
 
-qed_goal "IntD1" ZF.thy "!!c. c : A Int B ==> c : A"
+qed_goal "IntD1" thy "!!c. c : A Int B ==> c : A"
  (fn _ => [ Asm_full_simp_tac 1 ]);
 
-qed_goal "IntD2" ZF.thy "!!c. c : A Int B ==> c : B"
+qed_goal "IntD2" thy "!!c. c : A Int B ==> c : B"
  (fn _ => [ Asm_full_simp_tac 1 ]);
 
-qed_goal "IntE" ZF.thy
+qed_goal "IntE" thy
     "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P"
  (fn prems=>
   [ (resolve_tac prems 1),
@@ -108,21 +108,21 @@
 
 (*** Rules for set difference -- defined via Upair ***)
 
-qed_goalw "Diff_iff" ZF.thy [Diff_def] "c : A-B <-> (c:A & c~:B)"
+qed_goalw "Diff_iff" thy [Diff_def] "c : A-B <-> (c:A & c~:B)"
  (fn _ => [ Blast_tac 1 ]);
 
 Addsimps [Diff_iff];
 
-qed_goal "DiffI" ZF.thy "!!c. [| c : A;  c ~: B |] ==> c : A - B"
+qed_goal "DiffI" thy "!!c. [| c : A;  c ~: B |] ==> c : A - B"
  (fn _ => [ Asm_simp_tac 1 ]);
 
-qed_goal "DiffD1" ZF.thy "!!c. c : A - B ==> c : A"
+qed_goal "DiffD1" thy "!!c. c : A - B ==> c : A"
  (fn _ => [ Asm_full_simp_tac 1 ]);
 
-qed_goal "DiffD2" ZF.thy "!!c. c : A - B ==> c ~: B"
+qed_goal "DiffD2" thy "!!c. c : A - B ==> c ~: B"
  (fn _ => [ Asm_full_simp_tac 1 ]);
 
-qed_goal "DiffE" ZF.thy
+qed_goal "DiffE" thy
     "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P"
  (fn prems=>
   [ (resolve_tac prems 1),
@@ -133,27 +133,27 @@
 
 (*** Rules for cons -- defined via Un and Upair ***)
 
-qed_goalw "cons_iff" ZF.thy [cons_def] "a : cons(b,A) <-> (a=b | a:A)"
+qed_goalw "cons_iff" thy [cons_def] "a : cons(b,A) <-> (a=b | a:A)"
  (fn _ => [ Blast_tac 1 ]);
 
 Addsimps [cons_iff];
 
-qed_goal "consI1" ZF.thy "a : cons(a,B)"
+qed_goal "consI1" thy "a : cons(a,B)"
  (fn _ => [ Simp_tac 1 ]);
 
 Addsimps [consI1];
 
-qed_goal "consI2" ZF.thy "!!B. a : B ==> a : cons(b,B)"
+qed_goal "consI2" thy "!!B. a : B ==> a : cons(b,B)"
  (fn _ => [ Asm_simp_tac 1 ]);
 
-qed_goal "consE" ZF.thy
+qed_goal "consE" thy
     "[| a : cons(b,A);  a=b ==> P;  a:A ==> P |] ==> P"
  (fn major::prems=>
   [ (rtac (major RS (cons_iff RS iffD1 RS disjE)) 1),
     (REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ]);
 
 (*Stronger version of the rule above*)
-qed_goal "consE'" ZF.thy
+qed_goal "consE'" thy
     "[| a : cons(b,A);  a=b ==> P;  [| a:A;  a~=b |] ==> P |] ==> P"
  (fn major::prems =>
   [(rtac (major RS consE) 1),
@@ -164,14 +164,14 @@
    (etac notnotD 1)]);
 
 (*Classical introduction rule*)
-qed_goal "consCI" ZF.thy "(a~:B ==> a=b) ==> a: cons(b,B)"
+qed_goal "consCI" thy "(a~:B ==> a=b) ==> a: cons(b,B)"
  (fn prems=>
   [ Simp_tac 1, blast_tac (claset() addSIs prems) 1 ]);
 
 AddSIs [consCI];
 AddSEs [consE];
 
-qed_goal "cons_not_0" ZF.thy "cons(a,B) ~= 0"
+qed_goal "cons_not_0" thy "cons(a,B) ~= 0"
  (fn _ => [ (blast_tac (claset() addEs [equalityE]) 1) ]);
 
 bind_thm ("cons_neq_0", cons_not_0 RS notE);
@@ -181,10 +181,10 @@
 
 (*** Singletons - using cons ***)
 
-qed_goal "singleton_iff" ZF.thy "a : {b} <-> a=b"
+qed_goal "singleton_iff" thy "a : {b} <-> a=b"
  (fn _ => [ Simp_tac 1 ]);
 
-qed_goal "singletonI" ZF.thy "a : {a}"
+qed_goal "singletonI" thy "a : {a}"
  (fn _=> [ (rtac consI1 1) ]);
 
 bind_thm ("singletonE", make_elim (singleton_iff RS iffD1));
@@ -194,25 +194,25 @@
 
 (*** Rules for Descriptions ***)
 
-qed_goalw "the_equality" ZF.thy [the_def]
+qed_goalw "the_equality" thy [the_def]
     "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
  (fn [pa,eq] =>
   [ (fast_tac (claset() addSIs [pa] addEs [eq RS subst]) 1) ]);
 
 (* Only use this if you already know EX!x. P(x) *)
-qed_goal "the_equality2" ZF.thy
+qed_goal "the_equality2" thy
     "!!P. [| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
  (fn _ =>
   [ (deepen_tac (claset() addSIs [the_equality]) 1 1) ]);
 
-qed_goal "theI" ZF.thy "EX! x. P(x) ==> P(THE x. P(x))"
+qed_goal "theI" thy "EX! x. P(x) ==> P(THE x. P(x))"
  (fn [major]=>
   [ (rtac (major RS ex1E) 1),
     (resolve_tac [major RS the_equality2 RS ssubst] 1),
     (REPEAT (assume_tac 1)) ]);
 
 (*Easier to apply than theI: conclusion has only one occurrence of P*)
-qed_goal "theI2" ZF.thy
+qed_goal "theI2" thy
     "[| EX! x. P(x);  !!x. P(x) ==> Q(x) |] ==> Q(THE x. P(x))"
  (fn prems => [ resolve_tac prems 1, 
                 rtac theI 1, 
@@ -222,42 +222,42 @@
   (THE x.P(x))  rewrites to  (THE x. Q(x))  *)
 
 (*If it's "undefined", it's zero!*)
-qed_goalw "the_0" ZF.thy [the_def]
+qed_goalw "the_0" thy [the_def]
     "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
  (fn _ => [ (deepen_tac (claset() addSEs [ReplaceE]) 0 1) ]);
 
 
 (*** if -- a conditional expression for formulae ***)
 
-goalw ZF.thy [if_def] "if(True,a,b) = a";
+Goalw [if_def] "if(True,a,b) = a";
 by (blast_tac (claset() addSIs [the_equality]) 1);
 qed "if_true";
 
-goalw ZF.thy [if_def] "if(False,a,b) = b";
+Goalw [if_def] "if(False,a,b) = b";
 by (blast_tac (claset() addSIs [the_equality]) 1);
 qed "if_false";
 
 (*Never use with case splitting, or if P is known to be true or false*)
-val prems = goalw ZF.thy [if_def]
+val prems = Goalw [if_def]
     "[| P<->Q;  Q ==> a=c;  ~Q ==> b=d |] ==> if(P,a,b) = if(Q,c,d)";
 by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1);
 qed "if_cong";
 
 (*Not needed for rewriting, since P would rewrite to True anyway*)
-goalw ZF.thy [if_def] "!!P. P ==> if(P,a,b) = a";
+Goalw [if_def] "P ==> if(P,a,b) = a";
 by (blast_tac (claset() addSIs [the_equality]) 1);
 qed "if_P";
 
 (*Not needed for rewriting, since P would rewrite to False anyway*)
-goalw ZF.thy [if_def] "!!P. ~P ==> if(P,a,b) = b";
+Goalw [if_def] "~P ==> if(P,a,b) = b";
 by (blast_tac (claset() addSIs [the_equality]) 1);
 qed "if_not_P";
 
 Addsimps [if_true, if_false];
 
-qed_goal "split_if" ZF.thy
+qed_goal "split_if" thy
     "P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))"
- (fn _=> [ (excluded_middle_tac "Q" 1),
+ (fn _=> [ (case_tac "Q" 1),
            (Asm_simp_tac 1),
            (Asm_simp_tac 1) ]);
 
@@ -275,10 +275,10 @@
 		 split_if_mem1, split_if_mem2];
 
 (*Logically equivalent to split_if_mem2*)
-qed_goal "if_iff" ZF.thy "a: if(P,x,y) <-> P & a:x | ~P & a:y"
+qed_goal "if_iff" thy "a: if(P,x,y) <-> P & a:x | ~P & a:y"
  (fn _=> [ (simp_tac (simpset() addsplits [split_if]) 1) ]);
 
-qed_goal "if_type" ZF.thy
+qed_goal "if_type" thy
     "[| P ==> a: A;  ~P ==> b: A |] ==> if(P,a,b): A"
  (fn prems=> [ (simp_tac 
                 (simpset() addsimps prems addsplits [split_if]) 1) ]);
@@ -287,48 +287,48 @@
 (*** Foundation lemmas ***)
 
 (*was called mem_anti_sym*)
-qed_goal "mem_asym" ZF.thy "[| a:b;  ~P ==> b:a |] ==> P"
+qed_goal "mem_asym" thy "[| a:b;  ~P ==> b:a |] ==> P"
  (fn prems=>
   [ (rtac classical 1),
     (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1),
     REPEAT (blast_tac (claset() addIs prems addSEs [equalityE]) 1) ]);
 
 (*was called mem_anti_refl*)
-qed_goal "mem_irrefl" ZF.thy "a:a ==> P"
+qed_goal "mem_irrefl" thy "a:a ==> P"
  (fn [major]=> [ (rtac ([major,major] MRS mem_asym) 1) ]);
 
 (*mem_irrefl should NOT be added to default databases:
       it would be tried on most goals, making proofs slower!*)
 
-qed_goal "mem_not_refl" ZF.thy "a ~: a"
+qed_goal "mem_not_refl" thy "a ~: a"
  (K [ (rtac notI 1), (etac mem_irrefl 1) ]);
 
 (*Good for proving inequalities by rewriting*)
-qed_goal "mem_imp_not_eq" ZF.thy "!!a A. a:A ==> a ~= A"
+qed_goal "mem_imp_not_eq" thy "!!a A. a:A ==> a ~= A"
  (fn _=> [ blast_tac (claset() addSEs [mem_irrefl]) 1 ]);
 
 (*** Rules for succ ***)
 
-qed_goalw "succ_iff" ZF.thy [succ_def] "i : succ(j) <-> i=j | i:j"
+qed_goalw "succ_iff" thy [succ_def] "i : succ(j) <-> i=j | i:j"
  (fn _ => [ Blast_tac 1 ]);
 
-qed_goalw "succI1" ZF.thy [succ_def] "i : succ(i)"
+qed_goalw "succI1" thy [succ_def] "i : succ(i)"
  (fn _=> [ (rtac consI1 1) ]);
 
 Addsimps [succI1];
 
-qed_goalw "succI2" ZF.thy [succ_def]
+qed_goalw "succI2" thy [succ_def]
     "i : j ==> i : succ(j)"
  (fn [prem]=> [ (rtac (prem RS consI2) 1) ]);
 
-qed_goalw "succE" ZF.thy [succ_def]
+qed_goalw "succE" thy [succ_def]
     "[| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P"
  (fn major::prems=>
   [ (rtac (major RS consE) 1),
     (REPEAT (eresolve_tac prems 1)) ]);
 
 (*Classical introduction rule*)
-qed_goal "succCI" ZF.thy "(i~:j ==> i=j) ==> i: succ(j)"
+qed_goal "succCI" thy "(i~:j ==> i=j) ==> i: succ(j)"
  (fn [prem]=>
   [ (rtac (disjCI RS (succ_iff RS iffD2)) 1),
     (etac prem 1) ]);
@@ -336,7 +336,7 @@
 AddSIs [succCI];
 AddSEs [succE];
 
-qed_goal "succ_not_0" ZF.thy "succ(n) ~= 0"
+qed_goal "succ_not_0" thy "succ(n) ~= 0"
  (fn _=> [ (blast_tac (claset() addSEs [equalityE]) 1) ]);
 
 bind_thm ("succ_neq_0", succ_not_0 RS notE);
@@ -352,7 +352,7 @@
 bind_thm ("succ_neq_self", succI1 RS mem_imp_not_eq RS not_sym);
 
 
-qed_goal "succ_inject_iff" ZF.thy "succ(m) = succ(n) <-> m=n"
+qed_goal "succ_inject_iff" thy "succ(m) = succ(n) <-> m=n"
  (fn _=> [ (blast_tac (claset() addEs [mem_asym] addSEs [equalityE]) 1) ]);
 
 bind_thm ("succ_inject", succ_inject_iff RS iffD1);