# HG changeset patch
# User paulson
# Date 859988384 -7200
# Node ID 6476784dba1c62c6587a62294c5259c3d3a2e59d
# Parent  02c12d4c8b97ef13db39b5efff60a09e61ebd510
Converted to call blast_tac.
Proves theorems in ZF.thy to make that theory usable again

diff -r 02c12d4c8b97 -r 6476784dba1c src/ZF/ZF.ML
--- a/src/ZF/ZF.ML	Wed Apr 02 15:37:35 1997 +0200
+++ b/src/ZF/ZF.ML	Wed Apr 02 15:39:44 1997 +0200
@@ -54,7 +54,7 @@
 
 (*Trival rewrite rule;   (ALL x:A.P)<->P holds only if A is nonempty!*)
 qed_goal "ball_simp" ZF.thy "(ALL x:A. True) <-> True"
- (fn _=> [ Fast_tac 1 ]);
+ (fn _=> [ Blast_tac 1 ]);
 
 Addsimps [ball_simp];
 
@@ -67,7 +67,7 @@
 
 qed_goalw "bexI" ZF.thy [Bex_def]
     "!!P. [| P(x);  x: A |] ==> EX x:A. P(x)"
- (fn _=> [ Fast_tac 1 ]);
+ (fn _=> [ Blast_tac 1 ]);
 
 (*Not of the general form for such rules; ~EX has become ALL~ *)
 qed_goal "bexCI" ZF.thy 
@@ -124,21 +124,21 @@
 
 (*Sometimes useful with premises in this order*)
 qed_goal "rev_subsetD" ZF.thy "!!A B c. [| c:A; A<=B |] ==> c:B"
- (fn _=> [ Fast_tac 1 ]);
+ (fn _=> [ Blast_tac 1 ]);
 
 qed_goal "contra_subsetD" ZF.thy "!!c. [| A <= B; c ~: B |] ==> c ~: A"
- (fn _=> [ Fast_tac 1 ]);
+ (fn _=> [ Blast_tac 1 ]);
 
 qed_goal "rev_contra_subsetD" ZF.thy "!!c. [| c ~: B;  A <= B |] ==> c ~: A"
- (fn _=> [ Fast_tac 1 ]);
+ (fn _=> [ Blast_tac 1 ]);
 
 qed_goal "subset_refl" ZF.thy "A <= A"
- (fn _=> [ Fast_tac 1 ]);
+ (fn _=> [ Blast_tac 1 ]);
 
 Addsimps [subset_refl];
 
 qed_goal "subset_trans" ZF.thy "!!A B C. [| A<=B;  B<=C |] ==> A<=C"
- (fn _=> [ Fast_tac 1 ]);
+ (fn _=> [ Blast_tac 1 ]);
 
 (*Useful for proving A<=B by rewriting in some cases*)
 qed_goalw "subset_iff" ZF.thy [subset_def,Ball_def]
@@ -267,10 +267,10 @@
 
 qed_goalw "RepFun_iff" ZF.thy [Bex_def]
     "b : {f(x). x:A} <-> (EX x:A. b=f(x))"
- (fn _ => [Fast_tac 1]);
+ (fn _ => [Blast_tac 1]);
 
 goal ZF.thy "{x.x:A} = A";
-by (fast_tac (!claset) 1);
+by (Blast_tac 1);
 qed "triv_RepFun";
 
 Addsimps [RepFun_iff, triv_RepFun];
@@ -280,7 +280,7 @@
 (*Separation is derivable from Replacement*)
 qed_goalw "separation" ZF.thy [Collect_def]
     "a : {x:A. P(x)} <-> a:A & P(a)"
- (fn _=> [Fast_tac 1]);
+ (fn _=> [Blast_tac 1]);
 
 Addsimps [separation];
 
@@ -314,7 +314,7 @@
 
 (*The order of the premises presupposes that C is rigid; A may be flexible*)
 qed_goal "UnionI" ZF.thy "!!C. [| B: C;  A: B |] ==> A: Union(C)"
- (fn _=> [ Simp_tac 1, Fast_tac 1 ]);
+ (fn _=> [ Simp_tac 1, Blast_tac 1 ]);
 
 qed_goal "UnionE" ZF.thy
     "[| A : Union(C);  !!B.[| A: B;  B: C |] ==> R |] ==> R"
@@ -327,13 +327,13 @@
 
 qed_goalw "UN_iff" ZF.thy [Bex_def]
     "b : (UN x:A. B(x)) <-> (EX x:A. b : B(x))"
- (fn _=> [ Simp_tac 1, Fast_tac 1 ]);
+ (fn _=> [ Simp_tac 1, Blast_tac 1 ]);
 
 Addsimps [UN_iff];
 
 (*The order of the premises presupposes that A is rigid; b may be flexible*)
 qed_goal "UN_I" ZF.thy "!!A B. [| a: A;  b: B(a) |] ==> b: (UN x:A. B(x))"
- (fn _=> [ Simp_tac 1, Fast_tac 1 ]);
+ (fn _=> [ Simp_tac 1, Blast_tac 1 ]);
 
 qed_goal "UN_E" ZF.thy
     "[| b : (UN x:A. B(x));  !!x.[| x: A;  b: B(x) |] ==> R |] ==> R"
@@ -360,19 +360,19 @@
 (*Not obviously useful towards proving InterI, InterD, InterE*)
 qed_goalw "Inter_iff" ZF.thy [Inter_def,Ball_def]
     "A : Inter(C) <-> (ALL x:C. A: x) & (EX x. x:C)"
- (fn _=> [ Simp_tac 1, Fast_tac 1 ]);
+ (fn _=> [ Simp_tac 1, Blast_tac 1 ]);
 
 (* Intersection is well-behaved only if the family is non-empty! *)
 qed_goal "InterI" ZF.thy
     "[| !!x. x: C ==> A: x;  EX c. c:C |] ==> A : Inter(C)"
  (fn prems=> [ (simp_tac (!simpset addsimps [Inter_iff]) 1), 
-	       Cla.fast_tac (!claset addIs prems) 1 ]);
+	       blast_tac (!claset addIs prems) 1 ]);
 
 (*A "destruct" rule -- every B in C contains A as an element, but
   A:B can hold when B:C does not!  This rule is analogous to "spec". *)
 qed_goalw "InterD" ZF.thy [Inter_def]
     "!!C. [| A : Inter(C);  B : C |] ==> A : B"
- (fn _=> [ Fast_tac 1 ]);
+ (fn _=> [ Blast_tac 1 ]);
 
 (*"Classical" elimination rule -- does not require exhibiting B:C *)
 qed_goalw "InterE" ZF.thy [Inter_def]
@@ -393,7 +393,7 @@
 
 qed_goal "INT_I" ZF.thy
     "[| !!x. x: A ==> b: B(x);  a: A |] ==> b: (INT x:A. B(x))"
- (fn prems=> [ fast_tac (!claset addIs prems) 1 ]);
+ (fn prems=> [ blast_tac (!claset addIs prems) 1 ]);
 
 qed_goal "INT_E" ZF.thy
     "[| b : (INT x:A. B(x));  a: A |] ==> b : B(a)"
@@ -435,19 +435,19 @@
 AddSEs [emptyE];
 
 qed_goal "empty_subsetI" ZF.thy "0 <= A"
- (fn _=> [ Fast_tac 1 ]);
+ (fn _=> [ Blast_tac 1 ]);
 
 Addsimps [empty_subsetI];
 AddSIs [empty_subsetI];
 
 qed_goal "equals0I" ZF.thy "[| !!y. y:A ==> False |] ==> A=0"
- (fn prems=> [ fast_tac (!claset addDs prems) 1 ]);
+ (fn prems=> [ blast_tac (!claset addDs prems) 1 ]);
 
 qed_goal "equals0D" ZF.thy "!!P. [| A=0;  a:A |] ==> P"
- (fn _=> [ Full_simp_tac 1, Fast_tac 1 ]);
+ (fn _=> [ Full_simp_tac 1, Blast_tac 1 ]);
 
 qed_goal "not_emptyI" ZF.thy "!!A a. a:A ==> A ~= 0"
- (fn _=> [ Fast_tac 1 ]);
+ (fn _=> [ Blast_tac 1 ]);
 
 qed_goal "not_emptyE" ZF.thy "[| A ~= 0;  !!x. x:A ==> R |] ==> R"
  (fn [major,minor]=>
@@ -465,10 +465,10 @@
 (*The search is undirected; similar proof attempts may fail.
   b represents ANY map, such as (lam x:A.b(x)): A->Pow(A). *)
 qed_goal "cantor" ZF.thy "EX S: Pow(A). ALL x:A. b(x) ~= S"
- (fn _ => [Cla.best_tac cantor_cs 1]);
+ (fn _ => [best_tac cantor_cs 1]);
 
 (*Lemma for the inductive definition in Zorn.thy*)
 qed_goal "Union_in_Pow" ZF.thy
     "!!Y. Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)"
- (fn _ => [Fast_tac 1]);
+ (fn _ => [Blast_tac 1]);
 
diff -r 02c12d4c8b97 -r 6476784dba1c src/ZF/domrange.ML
--- a/src/ZF/domrange.ML	Wed Apr 02 15:37:35 1997 +0200
+++ b/src/ZF/domrange.ML	Wed Apr 02 15:39:44 1997 +0200
@@ -8,19 +8,19 @@
 
 (*** converse ***)
 
-qed_goalw "converse_iff" thy [converse_def]
+qed_goalw "converse_iff" ZF.thy [converse_def]
     "<a,b>: converse(r) <-> <b,a>:r"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
-qed_goalw "converseI" thy [converse_def]
+qed_goalw "converseI" ZF.thy [converse_def]
     "!!a b r. <a,b>:r ==> <b,a>:converse(r)"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
-qed_goalw "converseD" thy [converse_def]
+qed_goalw "converseD" ZF.thy [converse_def]
     "!!a b r. <a,b> : converse(r) ==> <b,a> : r"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
-qed_goalw "converseE" thy [converse_def]
+qed_goalw "converseE" ZF.thy [converse_def]
     "[| yx : converse(r);  \
 \       !!x y. [| yx=<y,x>;  <x,y>:r |] ==> P \
 \    |] ==> P"
@@ -34,31 +34,31 @@
 AddSIs [converseI];
 AddSEs [converseD,converseE];
 
-qed_goal "converse_converse" thy
+qed_goal "converse_converse" ZF.thy
     "!!A B r. r<=Sigma(A,B) ==> converse(converse(r)) = r"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
-qed_goal "converse_type" thy "!!A B r. r<=A*B ==> converse(r)<=B*A"
- (fn _ => [ (Fast_tac 1) ]);
+qed_goal "converse_type" ZF.thy "!!A B r. r<=A*B ==> converse(r)<=B*A"
+ (fn _ => [ (Blast_tac 1) ]);
 
-qed_goal "converse_prod" thy "converse(A*B) = B*A"
- (fn _ => [ (Fast_tac 1) ]);
+qed_goal "converse_prod" ZF.thy "converse(A*B) = B*A"
+ (fn _ => [ (Blast_tac 1) ]);
 
-qed_goal "converse_empty" thy "converse(0) = 0"
- (fn _ => [ (Fast_tac 1) ]);
+qed_goal "converse_empty" ZF.thy "converse(0) = 0"
+ (fn _ => [ (Blast_tac 1) ]);
 
 Addsimps [converse_prod, converse_empty];
 
 (*** domain ***)
 
-qed_goalw "domain_iff" thy [domain_def]
+qed_goalw "domain_iff" ZF.thy [domain_def]
     "a: domain(r) <-> (EX y. <a,y>: r)"
- (fn _=> [ (Fast_tac 1) ]);
+ (fn _=> [ (Blast_tac 1) ]);
 
-qed_goal "domainI" thy "!!a b r. <a,b>: r ==> a: domain(r)"
+qed_goal "domainI" ZF.thy "!!a b r. <a,b>: r ==> a: domain(r)"
  (fn _=> [ (etac (exI RS (domain_iff RS iffD2)) 1) ]);
 
-qed_goal "domainE" thy
+qed_goal "domainE" ZF.thy
     "[| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P"
  (fn prems=>
   [ (rtac (domain_iff RS iffD1 RS exE) 1),
@@ -67,15 +67,15 @@
 AddIs  [domainI];
 AddSEs [domainE];
 
-qed_goal "domain_subset" thy "domain(Sigma(A,B)) <= A"
- (fn _=> [ (Fast_tac 1) ]);
+qed_goal "domain_subset" ZF.thy "domain(Sigma(A,B)) <= A"
+ (fn _=> [ (Blast_tac 1) ]);
 
 (*** range ***)
 
-qed_goalw "rangeI" thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)"
+qed_goalw "rangeI" ZF.thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)"
  (fn _ => [ (etac (converseI RS domainI) 1) ]);
 
-qed_goalw "rangeE" thy [range_def]
+qed_goalw "rangeE" ZF.thy [range_def]
     "[| b : range(r);  !!x. <x,b>: r ==> P |] ==> P"
  (fn major::prems=>
   [ (rtac (major RS domainE) 1),
@@ -85,7 +85,7 @@
 AddIs  [rangeI];
 AddSEs [rangeE];
 
-qed_goalw "range_subset" thy [range_def] "range(A*B) <= B"
+qed_goalw "range_subset" ZF.thy [range_def] "range(A*B) <= B"
  (fn _ =>
   [ (stac converse_prod 1),
     (rtac domain_subset 1) ]);
@@ -93,17 +93,17 @@
 
 (*** field ***)
 
-qed_goalw "fieldI1" thy [field_def] "!!r. <a,b>: r ==> a : field(r)"
- (fn _ => [ (Fast_tac 1) ]);
+qed_goalw "fieldI1" ZF.thy [field_def] "!!r. <a,b>: r ==> a : field(r)"
+ (fn _ => [ (Blast_tac 1) ]);
 
-qed_goalw "fieldI2" thy [field_def] "!!r. <a,b>: r ==> b : field(r)"
- (fn _ => [ (Fast_tac 1) ]);
+qed_goalw "fieldI2" ZF.thy [field_def] "!!r. <a,b>: r ==> b : field(r)"
+ (fn _ => [ (Blast_tac 1) ]);
 
-qed_goalw "fieldCI" thy [field_def]
+qed_goalw "fieldCI" ZF.thy [field_def]
     "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"
- (fn [prem]=> [ (fast_tac (!claset addIs [prem]) 1) ]);
+ (fn [prem]=> [ (blast_tac (!claset addIs [prem]) 1) ]);
 
-qed_goalw "fieldE" thy [field_def]
+qed_goalw "fieldE" ZF.thy [field_def]
      "[| a : field(r);  \
 \        !!x. <a,x>: r ==> P;  \
 \        !!x. <x,a>: r ==> P        |] ==> P"
@@ -114,40 +114,40 @@
 AddIs  [fieldCI];
 AddSEs [fieldE];
 
-qed_goal "field_subset" thy "field(A*B) <= A Un B"
- (fn _ => [ (Fast_tac 1) ]);
+qed_goal "field_subset" ZF.thy "field(A*B) <= A Un B"
+ (fn _ => [ (Blast_tac 1) ]);
 
-qed_goalw "domain_subset_field" thy [field_def]
+qed_goalw "domain_subset_field" ZF.thy [field_def]
     "domain(r) <= field(r)"
  (fn _ => [ (rtac Un_upper1 1) ]);
 
-qed_goalw "range_subset_field" thy [field_def]
+qed_goalw "range_subset_field" ZF.thy [field_def]
     "range(r) <= field(r)"
  (fn _ => [ (rtac Un_upper2 1) ]);
 
-qed_goal "domain_times_range" thy
+qed_goal "domain_times_range" ZF.thy
     "!!A B r. r <= Sigma(A,B) ==> r <= domain(r)*range(r)"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
-qed_goal "field_times_field" thy
+qed_goal "field_times_field" ZF.thy
     "!!A B r. r <= Sigma(A,B) ==> r <= field(r)*field(r)"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 
 (*** Image of a set under a function/relation ***)
 
-qed_goalw "image_iff" thy [image_def] "b : r``A <-> (EX x:A. <x,b>:r)"
- (fn _ => [ (Fast_tac 1) ]);
+qed_goalw "image_iff" ZF.thy [image_def] "b : r``A <-> (EX x:A. <x,b>:r)"
+ (fn _ => [ (Blast_tac 1) ]);
 
-qed_goal "image_singleton_iff" thy    "b : r``{a} <-> <a,b>:r"
+qed_goal "image_singleton_iff" ZF.thy    "b : r``{a} <-> <a,b>:r"
  (fn _ => [ rtac (image_iff RS iff_trans) 1,
-            Fast_tac 1 ]);
+            Blast_tac 1 ]);
 
-qed_goalw "imageI" thy [image_def]
+qed_goalw "imageI" ZF.thy [image_def]
     "!!a b r. [| <a,b>: r;  a:A |] ==> b : r``A"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
-qed_goalw "imageE" thy [image_def]
+qed_goalw "imageE" ZF.thy [image_def]
     "[| b: r``A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P"
  (fn major::prems=>
   [ (rtac (major RS CollectE) 1),
@@ -156,32 +156,32 @@
 AddIs  [imageI];
 AddSEs [imageE];
 
-qed_goal "image_subset" thy "!!A B r. r <= A*B ==> r``C <= B"
- (fn _ => [ (Fast_tac 1) ]);
+qed_goal "image_subset" ZF.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" thy [vimage_def,image_def,converse_def]
+qed_goalw "vimage_iff" ZF.thy [vimage_def,image_def,converse_def]
     "a : r-``B <-> (EX y:B. <a,y>:r)"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
-qed_goal "vimage_singleton_iff" thy
+qed_goal "vimage_singleton_iff" ZF.thy
     "a : r-``{b} <-> <a,b>:r"
  (fn _ => [ rtac (vimage_iff RS iff_trans) 1,
-            Fast_tac 1 ]);
+            Blast_tac 1 ]);
 
-qed_goalw "vimageI" thy [vimage_def]
+qed_goalw "vimageI" ZF.thy [vimage_def]
     "!!A B r. [| <a,b>: r;  b:B |] ==> a : r-``B"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
-qed_goalw "vimageE" thy [vimage_def]
+qed_goalw "vimageE" ZF.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" thy [vimage_def]
+qed_goalw "vimage_subset" ZF.thy [vimage_def]
     "!!A B r. r <= A*B ==> r-``C <= A"
  (fn _ => [ (etac (converse_type RS image_subset) 1) ]);
 
@@ -194,22 +194,22 @@
 val ZF_cs = !claset delrules [equalityI];
 
 (** The Union of a set of relations is a relation -- Lemma for fun_Union **)
-goal thy "!!S. (ALL x:S. EX A B. x <= A*B) ==>  \
+goal ZF.thy "!!S. (ALL x:S. EX A B. x <= A*B) ==>  \
 \                 Union(S) <= domain(Union(S)) * range(Union(S))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "rel_Union";
 
 (** The Union of 2 relations is a relation (Lemma for fun_Un)  **)
-qed_goal "rel_Un" thy
+qed_goal "rel_Un" ZF.thy
     "!!r s. [| r <= A*B;  s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 
-goal thy "!!r. [| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)";
-by (Deepen_tac 0 1);
+goal ZF.thy "!!r. [| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)";
+by (Blast_tac 1);
 qed "domain_Diff_eq";
 
-goal thy "!!r. [| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)";
-by (Deepen_tac 0 1);
+goal ZF.thy "!!r. [| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)";
+by (Blast_tac 1);
 qed "range_Diff_eq";
 
diff -r 02c12d4c8b97 -r 6476784dba1c src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Wed Apr 02 15:37:35 1997 +0200
+++ b/src/ZF/equalities.ML	Wed Apr 02 15:39:44 1997 +0200
@@ -10,24 +10,24 @@
 (** Finite Sets **)
 
 (* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
-goal thy "{a} Un B = cons(a,B)";
-by (Fast_tac 1);
+goal ZF.thy "{a} Un B = cons(a,B)";
+by (Blast_tac 1);
 qed "cons_eq";
 
-goal thy "cons(a, cons(b, C)) = cons(b, cons(a, C))";
-by (Fast_tac 1);
+goal ZF.thy "cons(a, cons(b, C)) = cons(b, cons(a, C))";
+by (Blast_tac 1);
 qed "cons_commute";
 
-goal thy "!!B. a: B ==> cons(a,B) = B";
-by (Fast_tac 1);
+goal ZF.thy "!!B. a: B ==> cons(a,B) = B";
+by (Blast_tac 1);
 qed "cons_absorb";
 
-goal thy "!!B. a: B ==> cons(a, B-{a}) = B";
-by (Fast_tac 1);
+goal ZF.thy "!!B. a: B ==> cons(a, B-{a}) = B";
+by (Blast_tac 1);
 qed "cons_Diff";
 
-goal thy "!!C. [| a: C;  ALL y:C. y=b |] ==> C = {b}";
-by (Fast_tac 1);
+goal ZF.thy "!!C. [| 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,329 +35,329 @@
 (** Binary Intersection **)
 
 (*NOT an equality, but it seems to belong here...*)
-goal thy "cons(a,B) Int C <= cons(a, B Int C)";
-by (Fast_tac 1);
+goal ZF.thy "cons(a,B) Int C <= cons(a, B Int C)";
+by (Blast_tac 1);
 qed "Int_cons";
 
-goal thy "A Int A = A";
-by (Fast_tac 1);
+goal ZF.thy "A Int A = A";
+by (Blast_tac 1);
 qed "Int_absorb";
 
-goal thy "A Int B = B Int A";
-by (Fast_tac 1);
+goal ZF.thy "A Int B = B Int A";
+by (Blast_tac 1);
 qed "Int_commute";
 
-goal thy "(A Int B) Int C  =  A Int (B Int C)";
-by (Fast_tac 1);
+goal ZF.thy "(A Int B) Int C  =  A Int (B Int C)";
+by (Blast_tac 1);
 qed "Int_assoc";
 
-goal thy "(A Un B) Int C  =  (A Int C) Un (B Int C)";
-by (Fast_tac 1);
+goal ZF.thy "(A Un B) Int C  =  (A Int C) Un (B Int C)";
+by (Blast_tac 1);
 qed "Int_Un_distrib";
 
-goal thy "A<=B <-> A Int B = A";
-by (fast_tac (!claset addSEs [equalityE]) 1);
+goal ZF.thy "A<=B <-> A Int B = A";
+by (blast_tac (!claset addSEs [equalityE]) 1);
 qed "subset_Int_iff";
 
-goal thy "A<=B <-> B Int A = A";
-by (fast_tac (!claset addSEs [equalityE]) 1);
+goal ZF.thy "A<=B <-> B Int A = A";
+by (blast_tac (!claset addSEs [equalityE]) 1);
 qed "subset_Int_iff2";
 
-goal thy "!!A B C. C<=A ==> (A-B) Int C = C-B";
-by (Fast_tac 1);
+goal ZF.thy "!!A B C. C<=A ==> (A-B) Int C = C-B";
+by (Blast_tac 1);
 qed "Int_Diff_eq";
 
 (** Binary Union **)
 
-goal thy "cons(a,B) Un C = cons(a, B Un C)";
-by (Fast_tac 1);
+goal ZF.thy "cons(a,B) Un C = cons(a, B Un C)";
+by (Blast_tac 1);
 qed "Un_cons";
 
-goal thy "A Un A = A";
-by (Fast_tac 1);
+goal ZF.thy "A Un A = A";
+by (Blast_tac 1);
 qed "Un_absorb";
 
-goal thy "A Un B = B Un A";
-by (Fast_tac 1);
+goal ZF.thy "A Un B = B Un A";
+by (Blast_tac 1);
 qed "Un_commute";
 
-goal thy "(A Un B) Un C  =  A Un (B Un C)";
-by (Fast_tac 1);
+goal ZF.thy "(A Un B) Un C  =  A Un (B Un C)";
+by (Blast_tac 1);
 qed "Un_assoc";
 
-goal thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
-by (Fast_tac 1);
+goal ZF.thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
+by (Blast_tac 1);
 qed "Un_Int_distrib";
 
-goal thy "A<=B <-> A Un B = B";
-by (fast_tac (!claset addSEs [equalityE]) 1);
+goal ZF.thy "A<=B <-> A Un B = B";
+by (blast_tac (!claset addSEs [equalityE]) 1);
 qed "subset_Un_iff";
 
-goal thy "A<=B <-> B Un A = B";
-by (fast_tac (!claset addSEs [equalityE]) 1);
+goal ZF.thy "A<=B <-> B Un A = B";
+by (blast_tac (!claset addSEs [equalityE]) 1);
 qed "subset_Un_iff2";
 
 (** Simple properties of Diff -- set difference **)
 
-goal thy "A-A = 0";
-by (Fast_tac 1);
+goal ZF.thy "A-A = 0";
+by (Blast_tac 1);
 qed "Diff_cancel";
 
-goal thy "0-A = 0";
-by (Fast_tac 1);
+goal ZF.thy "0-A = 0";
+by (Blast_tac 1);
 qed "empty_Diff";
 
-goal thy "A-0 = A";
-by (Fast_tac 1);
+goal ZF.thy "A-0 = A";
+by (Blast_tac 1);
 qed "Diff_0";
 
-goal thy "A-B=0 <-> A<=B";
-by (fast_tac (!claset addEs [equalityE]) 1);
+goal ZF.thy "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 thy "A - cons(a,B) = A - B - {a}";
-by (Fast_tac 1);
+goal ZF.thy "A - cons(a,B) = A - B - {a}";
+by (Blast_tac 1);
 qed "Diff_cons";
 
 (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
-goal thy "A - cons(a,B) = A - {a} - B";
-by (Fast_tac 1);
+goal ZF.thy "A - cons(a,B) = A - {a} - B";
+by (Blast_tac 1);
 qed "Diff_cons2";
 
-goal thy "A Int (B-A) = 0";
-by (Fast_tac 1);
+goal ZF.thy "A Int (B-A) = 0";
+by (Blast_tac 1);
 qed "Diff_disjoint";
 
-goal thy "!!A B. A<=B ==> A Un (B-A) = B";
-by (Fast_tac 1);
+goal ZF.thy "!!A B. A<=B ==> A Un (B-A) = B";
+by (Blast_tac 1);
 qed "Diff_partition";
 
-goal thy "A <= B Un (A - B)";
-by (Fast_tac 1);
+goal ZF.thy "A <= B Un (A - B)";
+by (Blast_tac 1);
 qed "subset_Un_Diff";
 
-goal thy "!!A B. [| A<=B; B<=C |] ==> B-(C-A) = A";
-by (Fast_tac 1);
+goal ZF.thy "!!A B. [| A<=B; B<=C |] ==> B-(C-A) = A";
+by (Blast_tac 1);
 qed "double_complement";
 
-goal thy "(A Un B) - (B-A) = A";
-by (Fast_tac 1);
+goal ZF.thy "(A Un B) - (B-A) = A";
+by (Blast_tac 1);
 qed "double_complement_Un";
 
-goal thy
+goal ZF.thy
  "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Un_Int_crazy";
 
-goal thy "A - (B Un C) = (A-B) Int (A-C)";
-by (Fast_tac 1);
+goal ZF.thy "A - (B Un C) = (A-B) Int (A-C)";
+by (Blast_tac 1);
 qed "Diff_Un";
 
-goal thy "A - (B Int C) = (A-B) Un (A-C)";
-by (Fast_tac 1);
+goal ZF.thy "A - (B Int C) = (A-B) Un (A-C)";
+by (Blast_tac 1);
 qed "Diff_Int";
 
 (*Halmos, Naive Set Theory, page 16.*)
-goal thy "(A Int B) Un C = A Int (B Un C)  <->  C<=A";
-by (fast_tac (!claset addSEs [equalityE]) 1);
+goal ZF.thy "(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 thy "Union(cons(a,B)) = a Un Union(B)";
-by (Fast_tac 1);
+goal ZF.thy "Union(cons(a,B)) = a Un Union(B)";
+by (Blast_tac 1);
 qed "Union_cons";
 
-goal thy "Union(A Un B) = Union(A) Un Union(B)";
-by (Fast_tac 1);
+goal ZF.thy "Union(A Un B) = Union(A) Un Union(B)";
+by (Blast_tac 1);
 qed "Union_Un_distrib";
 
-goal thy "Union(A Int B) <= Union(A) Int Union(B)";
-by (Fast_tac 1);
+goal ZF.thy "Union(A Int B) <= Union(A) Int Union(B)";
+by (Blast_tac 1);
 qed "Union_Int_subset";
 
-goal thy "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)";
-by (fast_tac (!claset addSEs [equalityE]) 1);
+goal ZF.thy "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)";
+by (blast_tac (!claset addSEs [equalityE]) 1);
 qed "Union_disjoint";
 
-goalw thy [Inter_def] "Inter(0) = 0";
-by (Fast_tac 1);
+goalw ZF.thy [Inter_def] "Inter(0) = 0";
+by (Blast_tac 1);
 qed "Inter_0";
 
-goal thy "!!A B. [| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)";
-by (Fast_tac 1);
+goal ZF.thy "!!A B. [| 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 thy "!!A B. [| a:A;  b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)";
-by (Fast_tac 1);
+goal ZF.thy "!!A B. [| a:A;  b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)";
+by (Blast_tac 1);
 qed "Inter_Un_distrib";
 
-goal thy "Union({b}) = b";
-by (Fast_tac 1);
+goal ZF.thy "Union({b}) = b";
+by (Blast_tac 1);
 qed "Union_singleton";
 
-goal thy "Inter({b}) = b";
-by (Fast_tac 1);
+goal ZF.thy "Inter({b}) = b";
+by (Blast_tac 1);
 qed "Inter_singleton";
 
 (** Unions and Intersections of Families **)
 
-goal thy "Union(A) = (UN x:A. x)";
-by (Fast_tac 1);
+goal ZF.thy "Union(A) = (UN x:A. x)";
+by (Blast_tac 1);
 qed "Union_eq_UN";
 
-goalw thy [Inter_def] "Inter(A) = (INT x:A. x)";
-by (Fast_tac 1);
+goalw ZF.thy [Inter_def] "Inter(A) = (INT x:A. x)";
+by (Blast_tac 1);
 qed "Inter_eq_INT";
 
-goal thy "(UN i:0. A(i)) = 0";
-by (Fast_tac 1);
+goal ZF.thy "(UN i:0. A(i)) = 0";
+by (Blast_tac 1);
 qed "UN_0";
 
 (*Halmos, Naive Set Theory, page 35.*)
-goal thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
-by (Fast_tac 1);
+goal ZF.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
+by (Blast_tac 1);
 qed "Int_UN_distrib";
 
-goal thy "!!A B. i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
-by (Fast_tac 1);
+goal ZF.thy "!!A B. 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 thy
+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))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Int_UN_distrib2";
 
-goal thy
+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))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Un_INT_distrib2";
 
-goal thy "!!A. a: A ==> (UN y:A. c) = c";
-by (Fast_tac 1);
+goal ZF.thy "!!A. a: A ==> (UN y:A. c) = c";
+by (Blast_tac 1);
 qed "UN_constant";
 
-goal thy "!!A. a: A ==> (INT y:A. c) = c";
-by (Fast_tac 1);
+goal ZF.thy "!!A. a: A ==> (INT y:A. c) = c";
+by (Blast_tac 1);
 qed "INT_constant";
 
 (** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
     Union of a family of unions **)
 
-goal thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
-by (Fast_tac 1);
+goal ZF.thy "(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 thy
+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))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "INT_Int_distrib";
 
-goal thy "(UN z:I Int J. A(z)) <= (UN z:I. A(z)) Int (UN z:J. A(z))";
-by (Fast_tac 1);
+goal ZF.thy "(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 thy "!!A B. i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))";
-by (Fast_tac 1);
+goal ZF.thy "!!A B. i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))";
+by (Blast_tac 1);
 qed "Diff_UN";
 
-goal thy "!!A B. i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))";
-by (Fast_tac 1);
+goal ZF.thy "!!A B. 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 thy "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)";
-by (Fast_tac 1);
+goal ZF.thy "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 thy "A * cons(b,B) = A*{b} Un A*B";
-by (Fast_tac 1);
+goal ZF.thy "A * cons(b,B) = A*{b} Un A*B";
+by (Blast_tac 1);
 qed "Sigma_cons2";
 
-goal thy "Sigma(succ(A), B) = ({A}*B(A)) Un Sigma(A,B)";
-by (Fast_tac 1);
+goal ZF.thy "Sigma(succ(A), B) = ({A}*B(A)) Un Sigma(A,B)";
+by (Blast_tac 1);
 qed "Sigma_succ1";
 
-goal thy "A * succ(B) = A*{B} Un A*B";
-by (Fast_tac 1);
+goal ZF.thy "A * succ(B) = A*{B} Un A*B";
+by (Blast_tac 1);
 qed "Sigma_succ2";
 
-goal thy "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))";
-by (Fast_tac 1);
+goal ZF.thy "(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 thy "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))";
-by (Fast_tac 1);
+goal ZF.thy "(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 thy "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))";
-by (Fast_tac 1);
+goal ZF.thy "(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 thy "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))";
-by (Fast_tac 1);
+goal ZF.thy "(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 thy "I * (A Un B) = I*A Un I*B";
+goal ZF.thy "I * (A Un B) = I*A Un I*B";
 by (rtac SUM_Un_distrib2 1);
 qed "prod_Un_distrib2";
 
-goal thy "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))";
-by (Fast_tac 1);
+goal ZF.thy "(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 thy
+goal ZF.thy
     "(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "SUM_Int_distrib2";
 
 (*First-order version of the above, for rewriting*)
-goal thy "I * (A Int B) = I*A Int I*B";
+goal ZF.thy "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 thy "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))";
-by (Fast_tac 1);
+goal ZF.thy "(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" thy "!!A B. b:B ==> domain(A*B) = A"
- (fn _ => [ Fast_tac 1 ]);
+qed_goal "domain_of_prod" ZF.thy "!!A B. b:B ==> domain(A*B) = A"
+ (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "domain_0" thy "domain(0) = 0"
- (fn _ => [ Fast_tac 1 ]);
+qed_goal "domain_0" ZF.thy "domain(0) = 0"
+ (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "domain_cons" thy
+qed_goal "domain_cons" ZF.thy
     "domain(cons(<a,b>,r)) = cons(a, domain(r))"
- (fn _ => [ Fast_tac 1 ]);
+ (fn _ => [ Blast_tac 1 ]);
 
-goal thy "domain(A Un B) = domain(A) Un domain(B)";
-by (Fast_tac 1);
+goal ZF.thy "domain(A Un B) = domain(A) Un domain(B)";
+by (Blast_tac 1);
 qed "domain_Un_eq";
 
-goal thy "domain(A Int B) <= domain(A) Int domain(B)";
-by (Fast_tac 1);
+goal ZF.thy "domain(A Int B) <= domain(A) Int domain(B)";
+by (Blast_tac 1);
 qed "domain_Int_subset";
 
-goal thy "domain(A) - domain(B) <= domain(A - B)";
-by (Fast_tac 1);
+goal ZF.thy "domain(A) - domain(B) <= domain(A - B)";
+by (Blast_tac 1);
 qed "domain_Diff_subset";
 
-goal thy "domain(converse(r)) = range(r)";
-by (Fast_tac 1);
+goal ZF.thy "domain(converse(r)) = range(r)";
+by (Blast_tac 1);
 qed "domain_converse";
 
 Addsimps [domain_0, domain_cons, domain_Un_eq, domain_converse];
@@ -365,31 +365,31 @@
 
 (** Range **)
 
-qed_goal "range_of_prod" thy
+qed_goal "range_of_prod" ZF.thy
     "!!a A B. a:A ==> range(A*B) = B"
- (fn _ => [ Fast_tac 1 ]);
+ (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "range_0" thy "range(0) = 0"
- (fn _ => [ Fast_tac 1 ]); 
+qed_goal "range_0" ZF.thy "range(0) = 0"
+ (fn _ => [ Blast_tac 1 ]); 
 
-qed_goal "range_cons" thy
+qed_goal "range_cons" ZF.thy
     "range(cons(<a,b>,r)) = cons(b, range(r))"
- (fn _ => [ Fast_tac 1 ]);
+ (fn _ => [ Blast_tac 1 ]);
 
-goal thy "range(A Un B) = range(A) Un range(B)";
-by (Fast_tac 1);
+goal ZF.thy "range(A Un B) = range(A) Un range(B)";
+by (Blast_tac 1);
 qed "range_Un_eq";
 
-goal thy "range(A Int B) <= range(A) Int range(B)";
-by (Fast_tac 1);
+goal ZF.thy "range(A Int B) <= range(A) Int range(B)";
+by (Blast_tac 1);
 qed "range_Int_subset";
 
-goal thy "range(A) - range(B) <= range(A - B)";
-by (Fast_tac 1);
+goal ZF.thy "range(A) - range(B) <= range(A - B)";
+by (Blast_tac 1);
 qed "range_Diff_subset";
 
-goal thy "range(converse(r)) = domain(r)";
-by (Fast_tac 1);
+goal ZF.thy "range(converse(r)) = domain(r)";
+by (Blast_tac 1);
 qed "range_converse";
 
 Addsimps [range_0, range_cons, range_Un_eq, range_converse];
@@ -397,30 +397,30 @@
 
 (** Field **)
 
-qed_goal "field_of_prod" thy "field(A*A) = A"
- (fn _ => [ Fast_tac 1 ]); 
+qed_goal "field_of_prod" ZF.thy "field(A*A) = A"
+ (fn _ => [ Blast_tac 1 ]); 
 
-qed_goal "field_0" thy "field(0) = 0"
- (fn _ => [ Fast_tac 1 ]); 
+qed_goal "field_0" ZF.thy "field(0) = 0"
+ (fn _ => [ Blast_tac 1 ]); 
 
-qed_goal "field_cons" thy
+qed_goal "field_cons" ZF.thy
     "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
- (fn _ => [ rtac equalityI 1, ALLGOALS (Fast_tac) ]);
+ (fn _ => [ rtac equalityI 1, ALLGOALS (Blast_tac) ]);
 
-goal thy "field(A Un B) = field(A) Un field(B)";
-by (Fast_tac 1);
+goal ZF.thy "field(A Un B) = field(A) Un field(B)";
+by (Blast_tac 1);
 qed "field_Un_eq";
 
-goal thy "field(A Int B) <= field(A) Int field(B)";
-by (Fast_tac 1);
+goal ZF.thy "field(A Int B) <= field(A) Int field(B)";
+by (Blast_tac 1);
 qed "field_Int_subset";
 
-goal thy "field(A) - field(B) <= field(A - B)";
-by (Fast_tac 1);
+goal ZF.thy "field(A) - field(B) <= field(A - B)";
+by (Blast_tac 1);
 qed "field_Diff_subset";
 
-goal thy "field(converse(r)) = field(r)";
-by (Fast_tac 1);
+goal ZF.thy "field(converse(r)) = field(r)";
+by (Blast_tac 1);
 qed "field_converse";
 
 Addsimps [field_0, field_cons, field_Un_eq, field_converse];
@@ -428,24 +428,24 @@
 
 (** Image **)
 
-goal thy "r``0 = 0";
-by (Fast_tac 1);
+goal ZF.thy "r``0 = 0";
+by (Blast_tac 1);
 qed "image_0";
 
-goal thy "r``(A Un B) = (r``A) Un (r``B)";
-by (Fast_tac 1);
+goal ZF.thy "r``(A Un B) = (r``A) Un (r``B)";
+by (Blast_tac 1);
 qed "image_Un";
 
-goal thy "r``(A Int B) <= (r``A) Int (r``B)";
-by (Fast_tac 1);
+goal ZF.thy "r``(A Int B) <= (r``A) Int (r``B)";
+by (Blast_tac 1);
 qed "image_Int_subset";
 
-goal thy "(r Int A*A)``B <= (r``B) Int A";
-by (Fast_tac 1);
+goal ZF.thy "(r Int A*A)``B <= (r``B) Int A";
+by (Blast_tac 1);
 qed "image_Int_square_subset";
 
-goal thy "!!r. B<=A ==> (r Int A*A)``B = (r``B) Int A";
-by (Fast_tac 1);
+goal ZF.thy "!!r. B<=A ==> (r Int A*A)``B = (r``B) Int A";
+by (Blast_tac 1);
 qed "image_Int_square";
 
 Addsimps [image_0, image_Un];
@@ -453,24 +453,24 @@
 
 (** Inverse Image **)
 
-goal thy "r-``0 = 0";
-by (Fast_tac 1);
+goal ZF.thy "r-``0 = 0";
+by (Blast_tac 1);
 qed "vimage_0";
 
-goal thy "r-``(A Un B) = (r-``A) Un (r-``B)";
-by (Fast_tac 1);
+goal ZF.thy "r-``(A Un B) = (r-``A) Un (r-``B)";
+by (Blast_tac 1);
 qed "vimage_Un";
 
-goal thy "r-``(A Int B) <= (r-``A) Int (r-``B)";
-by (Fast_tac 1);
+goal ZF.thy "r-``(A Int B) <= (r-``A) Int (r-``B)";
+by (Blast_tac 1);
 qed "vimage_Int_subset";
 
-goal thy "(r Int A*A)-``B <= (r-``B) Int A";
-by (Fast_tac 1);
+goal ZF.thy "(r Int A*A)-``B <= (r-``B) Int A";
+by (Blast_tac 1);
 qed "vimage_Int_square_subset";
 
-goal thy "!!r. B<=A ==> (r Int A*A)-``B = (r-``B) Int A";
-by (Fast_tac 1);
+goal ZF.thy "!!r. B<=A ==> (r Int A*A)-``B = (r-``B) Int A";
+by (Blast_tac 1);
 qed "vimage_Int_square";
 
 Addsimps [vimage_0, vimage_Un];
@@ -478,79 +478,80 @@
 
 (** Converse **)
 
-goal thy "converse(A Un B) = converse(A) Un converse(B)";
-by (Fast_tac 1);
+goal ZF.thy "converse(A Un B) = converse(A) Un converse(B)";
+by (Blast_tac 1);
 qed "converse_Un";
 
-goal thy "converse(A Int B) = converse(A) Int converse(B)";
-by (Fast_tac 1);
+goal ZF.thy "converse(A Int B) = converse(A) Int converse(B)";
+by (Blast_tac 1);
 qed "converse_Int";
 
-goal thy "converse(A - B) = converse(A) - converse(B)";
-by (Fast_tac 1);
+goal ZF.thy "converse(A - B) = converse(A) - converse(B)";
+by (Blast_tac 1);
 qed "converse_Diff";
 
-goal thy "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))";
-by (Fast_tac 1);
+goal ZF.thy "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))";
+by (Blast_tac 1);
 qed "converse_UN";
 
 (*Unfolding Inter avoids using excluded middle on A=0*)
-goalw thy [Inter_def] "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))";
-by (Fast_tac 1);
+goalw ZF.thy [Inter_def] "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))";
+by (Blast_tac 1);
 qed "converse_INT";
 
 Addsimps [converse_Un, converse_Int, converse_Diff, converse_UN, converse_INT];
 
 (** Pow **)
 
-goal thy "Pow(A) Un Pow(B) <= Pow(A Un B)";
-by (Fast_tac 1);
+goal ZF.thy "Pow(A) Un Pow(B) <= Pow(A Un B)";
+by (Blast_tac 1);
 qed "Un_Pow_subset";
 
-goal thy "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))";
-by (Fast_tac 1);
+goal ZF.thy "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))";
+by (Blast_tac 1);
 qed "UN_Pow_subset";
 
-goal thy "A <= Pow(Union(A))";
-by (Fast_tac 1);
+goal ZF.thy "A <= Pow(Union(A))";
+by (Blast_tac 1);
 qed "subset_Pow_Union";
 
-goal thy "Union(Pow(A)) = A";
-by (Fast_tac 1);
+goal ZF.thy "Union(Pow(A)) = A";
+by (Blast_tac 1);
 qed "Union_Pow_eq";
 
-goal thy "Pow(A Int B) = Pow(A) Int Pow(B)";
-by (Fast_tac 1);
+goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
+by (Blast_tac 1);
 qed "Int_Pow_eq";
 
-goal thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
-by (Fast_tac 1);
+goal ZF.thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
+by (Blast_tac 1);
 qed "INT_Pow_subset";
 
 Addsimps [Union_Pow_eq, Int_Pow_eq];
 
 (** RepFun **)
 
-goal thy "{f(x).x:A}=0 <-> A=0";
-by (fast_tac (!claset addSEs [equalityE]) 1);
+goal ZF.thy "{f(x).x:A}=0 <-> A=0";
+	(*blast_tac takes too long to search depth 5*)
+by (Blast.depth_tac (!claset addSEs [equalityE]) 6 1);
 qed "RepFun_eq_0_iff";
 
 (** Collect **)
 
-goal thy "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)";
-by (Fast_tac 1);
+goal ZF.thy "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)";
+by (Blast_tac 1);
 qed "Collect_Un";
 
-goal thy "Collect(A Int B, P) = Collect(A,P) Int Collect(B,P)";
-by (Fast_tac 1);
+goal ZF.thy "Collect(A Int B, P) = Collect(A,P) Int Collect(B,P)";
+by (Blast_tac 1);
 qed "Collect_Int";
 
-goal thy "Collect(A - B, P) = Collect(A,P) - Collect(B,P)";
-by (Fast_tac 1);
+goal ZF.thy "Collect(A - B, P) = Collect(A,P) - Collect(B,P)";
+by (Blast_tac 1);
 qed "Collect_Diff";
 
-goal thy "{x:cons(a,B). P(x)} = if(P(a), cons(a, {x:B. P(x)}), {x:B. P(x)})";
+goal ZF.thy "{x:cons(a,B). P(x)} = if(P(a), cons(a, {x:B. P(x)}), {x:B. P(x)})";
 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Collect_cons";
 
diff -r 02c12d4c8b97 -r 6476784dba1c src/ZF/func.ML
--- a/src/ZF/func.ML	Wed Apr 02 15:37:35 1997 +0200
+++ b/src/ZF/func.ML	Wed Apr 02 15:39:44 1997 +0200
@@ -8,36 +8,32 @@
 
 (*** The Pi operator -- dependent function space ***)
 
-goalw thy [Pi_def]
+goalw ZF.thy [Pi_def]
     "f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Pi_iff";
 
 (*For upward compatibility with the former definition*)
-goalw thy [Pi_def, function_def]
+goalw ZF.thy [Pi_def, function_def]
     "f: Pi(A,B) <-> f<=Sigma(A,B) & (ALL x:A. EX! y. <x,y>: f)";
-by (safe_tac (!claset));
-by (Best_tac 1);
-by (Best_tac 1);
-by (set_mp_tac 1);
-by (Deepen_tac 3 1);
+by (Blast_tac 1);
 qed "Pi_iff_old";
 
-goal thy "!!f. f: Pi(A,B) ==> function(f)";
+goal ZF.thy "!!f. 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 thy [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)";  
+val [major] = goalw ZF.thy [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)";  
 by (rtac (major RS CollectD1 RS PowD) 1);
 qed "fun_is_rel";
 
-goal thy "!!f. [| f: Pi(A,B);  a:A |] ==> EX! y. <a,y>: f";  
-by (fast_tac (!claset addSDs [Pi_iff_old RS iffD1]) 1);
+goal ZF.thy "!!f. [| 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 thy [Pi_def]
+val prems = goalw ZF.thy [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";
@@ -47,101 +43,101 @@
   Sigmas and Pis are abbreviated as * or -> *)
 
 (*Weakening one function type to another; see also Pi_type*)
-goalw thy [Pi_def] "!!f. [| f: A->B;  B<=D |] ==> f: A->D";
+goalw ZF.thy [Pi_def] "!!f. [| f: A->B;  B<=D |] ==> f: A->D";
 by (Best_tac 1);
 qed "fun_weaken_type";
 
 (*Empty function spaces*)
-goalw thy [Pi_def, function_def] "Pi(0,A) = {0}";
-by (Fast_tac 1);
+goalw ZF.thy [Pi_def, function_def] "Pi(0,A) = {0}";
+by (Blast_tac 1);
 qed "Pi_empty1";
 
-goalw thy [Pi_def] "!!A a. a:A ==> A->0 = 0";
-by (Fast_tac 1);
+goalw ZF.thy [Pi_def] "!!A a. a:A ==> A->0 = 0";
+by (Blast_tac 1);
 qed "Pi_empty2";
 
 (*The empty function*)
-goalw thy [Pi_def, function_def] "0: Pi(0,B)";
-by (Fast_tac 1);
+goalw ZF.thy [Pi_def, function_def] "0: Pi(0,B)";
+by (Blast_tac 1);
 qed "empty_fun";
 
 (*The singleton function*)
-goalw thy [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
-by (Fast_tac 1);
+goalw ZF.thy [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
+by (Blast_tac 1);
 qed "singleton_fun";
 
 Addsimps [empty_fun, singleton_fun];
 
 (*** Function Application ***)
 
-goalw thy [Pi_def, function_def]
+goalw ZF.thy [Pi_def, function_def]
      "!!a b f. [| <a,b>: f;  <a,c>: f;  f: Pi(A,B) |] ==> b=c";
-by (Deepen_tac 3 1);
+by (Blast_tac 1);
 qed "apply_equality2";
 
-goalw thy [apply_def] "!!a b f. [| <a,b>: f;  f: Pi(A,B) |] ==> f`a = b";
+goalw ZF.thy [apply_def] "!!a b f. [| <a,b>: f;  f: Pi(A,B) |] ==> f`a = b";
 by (rtac the_equality 1);
 by (rtac apply_equality2 2);
 by (REPEAT (assume_tac 1));
 qed "apply_equality";
 
 (*Applying a function outside its domain yields 0*)
-goalw thy [apply_def]
+goalw ZF.thy [apply_def]
     "!!a b f. [| a ~: domain(f);  f: Pi(A,B) |] ==> f`a = 0";
 by (rtac the_0 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "apply_0";
 
-goal thy "!!f. [| f: Pi(A,B);  c: f |] ==> EX x:A.  c = <x,f`x>";
+goal ZF.thy "!!f. [| f: Pi(A,B);  c: f |] ==> EX x:A.  c = <x,f`x>";
 by (forward_tac [fun_is_rel] 1);
-by (fast_tac (!claset addDs [apply_equality]) 1);
+by (blast_tac (!claset addDs [apply_equality]) 1);
 qed "Pi_memberD";
 
-goal thy "!!f. [| f: Pi(A,B);  a:A |] ==> <a,f`a>: f";
+goal ZF.thy "!!f. [| 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 thy "!!f. [| f: Pi(A,B);  a:A |] ==> f`a : B(a)"; 
+goal ZF.thy "!!f. [| 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 thy "!!f. [| f: A->B;  a:A |] ==> f`a : B"; 
+goal ZF.thy "!!f. [| f: A->B;  a:A |] ==> f`a : B"; 
 by (REPEAT (ares_tac [apply_type] 1));
 qed "apply_funtype";
 
-val [major] = goal thy
+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 (fast_tac (!claset addSIs [major RS apply_Pair, 
+by (blast_tac (!claset addSIs [major RS apply_Pair, 
 			      major RSN (2,apply_equality)]) 1);
 qed "apply_iff";
 
 (*Refining one Pi type to another*)
-val pi_prem::prems = goal thy
+val pi_prem::prems = goal ZF.thy
     "[| 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);
-by (fast_tac (!claset addIs prems addSDs [pi_prem RS Pi_memberD]) 1);
+by (blast_tac (!claset addIs prems addSDs [pi_prem RS Pi_memberD]) 1);
 qed "Pi_type";
 
 
 (** Elimination of membership in a function **)
 
-goal thy "!!a A. [| <a,b> : f;  f: Pi(A,B) |] ==> a : A";
+goal ZF.thy "!!a A. [| <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 thy "!!b B a. [| <a,b> : f;  f: Pi(A,B) |] ==> b : B(a)";
+goal ZF.thy "!!b B a. [| <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 thy
+val prems = goal ZF.thy
     "[| <a,b>: f;  f: Pi(A,B);       \
 \       [| a:A;  b:B(a);  f`a = b |] ==> P  \
 \    |] ==> P";
@@ -152,49 +148,49 @@
 
 (*** Lambda Abstraction ***)
 
-goalw thy [lam_def] "!!A b. a:A ==> <a,b(a)> : (lam x:A. b(x))";  
+goalw ZF.thy [lam_def] "!!A b. a:A ==> <a,b(a)> : (lam x:A. b(x))";  
 by (etac RepFunI 1);
 qed "lamI";
 
-val major::prems = goalw thy [lam_def]
+val major::prems = goalw ZF.thy [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 thy "!!a b c. [| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)";  
+goal ZF.thy "!!a b c. [| <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 thy [lam_def, Pi_def, function_def]
+val prems = goalw ZF.thy [lam_def, Pi_def, function_def]
     "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A.b(x)) : Pi(A,B)";  
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
 qed "lam_type";
 
-goal thy "(lam x:A.b(x)) : A -> {b(x). x:A}";
+goal ZF.thy "(lam x:A.b(x)) : A -> {b(x). x:A}";
 by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1));
 qed "lam_funtype";
 
-goal thy "!!a A. a : A ==> (lam x:A.b(x)) ` a = b(a)";
+goal ZF.thy "!!a A. a : A ==> (lam x:A.b(x)) ` a = b(a)";
 by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1));
 qed "beta";
 
-goalw thy [lam_def] "(lam x:0. b(x)) = 0";
+goalw ZF.thy [lam_def] "(lam x:0. b(x)) = 0";
 by (Simp_tac 1);
 qed "lam_empty";
 
 Addsimps [beta, lam_empty];
 
 (*congruence rule for lambda abstraction*)
-val prems = goalw thy [lam_def] 
+val prems = goalw ZF.thy [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 thy
+val [major] = goal ZF.thy
     "(!!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);
@@ -207,7 +203,7 @@
 (** Extensionality **)
 
 (*Semi-extensionality!*)
-val prems = goal thy
+val prems = goal ZF.thy
     "[| f : Pi(A,B);  g: Pi(C,D);  A<=C; \
 \       !!x. x:A ==> f`x = g`x       |] ==> f<=g";
 by (rtac subsetI 1);
@@ -217,14 +213,14 @@
 by (REPEAT (ares_tac (prems@[apply_Pair,subsetD]) 1));
 qed "fun_subset";
 
-val prems = goal thy
+val prems = goal ZF.thy
     "[| 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 thy "!!f A B. f : Pi(A,B) ==> (lam x:A. f`x) = f";
+goal ZF.thy "!!f A B. 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";
@@ -232,7 +228,7 @@
 Addsimps [eta];
 
 (*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
-val prems = goal thy
+val prems = goal ZF.thy
     "[| f: Pi(A,B);        \
 \       !!b. [| ALL x:A. b(x):B(x);  f = (lam x:A.b(x)) |] ==> P   \
 \    |] ==> P";
@@ -244,11 +240,11 @@
 
 (** Images of functions **)
 
-goalw thy [lam_def] "!!C A. C <= A ==> (lam x:A.b(x)) `` C = {b(x). x:C}";
-by (Fast_tac 1);
+goalw ZF.thy [lam_def] "!!C A. C <= A ==> (lam x:A.b(x)) `` C = {b(x). x:C}";
+by (Blast_tac 1);
 qed "image_lam";
 
-goal thy "!!C A. [| f : Pi(A,B);  C <= A |] ==> f``C = {f`x. x:C}";
+goal ZF.thy "!!C A. [| 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);
@@ -257,44 +253,44 @@
 
 (*** properties of "restrict" ***)
 
-goalw thy [restrict_def,lam_def]
+goalw ZF.thy [restrict_def,lam_def]
     "!!f A. [| f: Pi(C,B);  A<=C |] ==> restrict(f,A) <= f";
-by (fast_tac (!claset addIs [apply_Pair]) 1);
+by (blast_tac (!claset addIs [apply_Pair]) 1);
 qed "restrict_subset";
 
-val prems = goalw thy [restrict_def]
+val prems = goalw ZF.thy [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 thy 
+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);
 qed "restrict_type2";
 
-goalw thy [restrict_def] "!!a A. a : A ==> restrict(f,A) ` a = f`a";
+goalw ZF.thy [restrict_def] "!!a A. a : A ==> restrict(f,A) ` a = f`a";
 by (etac beta 1);
 qed "restrict";
 
-goalw thy [restrict_def] "restrict(f,0) = 0";
+goalw ZF.thy [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 thy [restrict_def]
+val prems = goalw ZF.thy [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 thy [restrict_def, lam_def] "domain(restrict(f,C)) = C";
-by (Fast_tac 1);
+goalw ZF.thy [restrict_def, lam_def] "domain(restrict(f,C)) = C";
+by (Blast_tac 1);
 qed "domain_restrict";
 
-val [prem] = goalw thy [restrict_def]
+val [prem] = goalw ZF.thy [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*)
@@ -306,18 +302,18 @@
 
 (** The Union of a set of COMPATIBLE functions is a function **)
 
-goalw thy [function_def]
+goalw ZF.thy [function_def]
     "!!S. [| ALL x:S. function(x); \
 \            ALL x:S. ALL y:S. x<=y | y<=x  |] ==>  \
 \         function(Union(S))";
-by (fast_tac (!claset addSDs [bspec RS bspec]) 1);
+by (blast_tac (!claset addSDs [bspec RS bspec]) 1);
 qed "function_Union";
 
-goalw thy [Pi_def]
+goalw ZF.thy [Pi_def]
     "!!S. [| 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 (fast_tac (subset_cs addSIs [rel_Union, function_Union]) 1);
+by (blast_tac (subset_cs addSIs [rel_Union, function_Union]) 1);
 qed "fun_Union";
 
 
@@ -327,30 +323,24 @@
               Un_upper1 RSN (2, subset_trans), 
               Un_upper2 RSN (2, subset_trans)];
 
-goal thy
+goal ZF.thy
     "!!f. [| f: A->B;  g: C->D;  A Int C = 0  |] ==>  \
 \         (f Un g) : (A Un C) -> (B Un D)";
-(*Solve the product and domain subgoals using distributive laws*)
-by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff,extension]@Un_rls) 1);
-by (asm_simp_tac (FOL_ss addsimps [function_def]) 1);
+(*Prove the product and domain subgoals using distributive laws*)
+by (asm_full_simp_tac (!simpset addsimps [Pi_iff,extension]@Un_rls) 1);
 by (safe_tac (!claset));
-(*Solve the two cases that contradict A Int C = 0*)
-by (Deepen_tac 2 2);
-by (Deepen_tac 2 2);
 by (rewtac function_def);
-by (REPEAT_FIRST (dtac (spec RS spec)));
-by (Deepen_tac 1 1);
-by (Deepen_tac 1 1);
+by (Blast.depth_tac (!claset) 8 1);
 qed "fun_disjoint_Un";
 
-goal thy
+goal ZF.thy
     "!!f g a. [| 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 thy
+goal ZF.thy
     "!!f g c. [| 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);
@@ -359,41 +349,41 @@
 
 (** Domain and range of a function/relation **)
 
-goalw thy [Pi_def] "!!f. f : Pi(A,B) ==> domain(f)=A";
-by (Fast_tac 1);
+goalw ZF.thy [Pi_def] "!!f. f : Pi(A,B) ==> domain(f)=A";
+by (Blast_tac 1);
 qed "domain_of_fun";
 
-goal thy "!!f. [| f : Pi(A,B);  a: A |] ==> f`a : range(f)";
+goal ZF.thy "!!f. [| 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 thy "f : Pi(A,B) ==> f : A->range(f)";
+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);
 qed "range_of_fun";
 
 (*** Extensions of functions ***)
 
-goal thy
+goal ZF.thy
     "!!f A B. [| 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 (Fast_tac 1);
+by (Blast_tac 1);
 qed "fun_extend";
 
-goal thy
+goal ZF.thy
     "!!f A B. [| f: A->B;  c~:A;  b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B";
-by (fast_tac (!claset addEs [fun_extend RS fun_weaken_type]) 1);
+by (blast_tac (!claset addIs [fun_extend RS fun_weaken_type]) 1);
 qed "fun_extend3";
 
-goal thy "!!f A B. [| f: A->B;  a:A;  c~:A |] ==> cons(<c,b>,f)`a = f`a";
+goal ZF.thy "!!f A B. [| 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 thy "!!f A B. [| f: A->B;  c~:A |] ==> cons(<c,b>,f)`c = b";
+goal ZF.thy "!!f A B. [| 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));
@@ -403,13 +393,13 @@
 Addsimps [singleton_apply];
 
 (*For Finite.ML.  Inclusion of right into left is easy*)
-goal thy
+goal ZF.thy
     "!!c. 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*)
 by (subgoal_tac "restrict(x, A) : A -> B" 1);
-by (fast_tac (!claset addEs [restrict_type2]) 2);
+by (blast_tac (!claset addIs [restrict_type2]) 2);
 by (rtac UN_I 1 THEN assume_tac 1);
 by (rtac (apply_funtype RS UN_I) 1 THEN REPEAT (ares_tac [consI1] 1));
 by (Simp_tac 1);
diff -r 02c12d4c8b97 -r 6476784dba1c src/ZF/pair.ML
--- a/src/ZF/pair.ML	Wed Apr 02 15:37:35 1997 +0200
+++ b/src/ZF/pair.ML	Wed Apr 02 15:39:44 1997 +0200
@@ -8,20 +8,20 @@
 
 (** Lemmas for showing that <a,b> uniquely determines a and b **)
 
-qed_goal "singleton_eq_iff" thy
+qed_goal "singleton_eq_iff" ZF.thy
     "{a} = {b} <-> a=b"
  (fn _=> [ (resolve_tac [extension RS iff_trans] 1),
-           (Fast_tac 1) ]);
+           (Blast_tac 1) ]);
 
-qed_goal "doubleton_eq_iff" thy
+qed_goal "doubleton_eq_iff" ZF.thy
     "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"
  (fn _=> [ (resolve_tac [extension RS iff_trans] 1),
-           (Fast_tac 1) ]);
+           (Blast_tac 1) ]);
 
-qed_goalw "Pair_iff" thy [Pair_def]
+qed_goalw "Pair_iff" ZF.thy [Pair_def]
     "<a,b> = <c,d> <-> a=c & b=d"
  (fn _=> [ (simp_tac (!simpset addsimps [doubleton_eq_iff]) 1),
-           (Fast_tac 1) ]);
+           (Blast_tac 1) ]);
 
 Addsimps [Pair_iff];
 
@@ -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" thy [Pair_def] "<a,b> ~= 0"
- (fn _ => [ (fast_tac (!claset addEs [equalityE]) 1) ]);
+qed_goalw "Pair_not_0" ZF.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" thy [Pair_def] "<a,b>=a ==> P"
+qed_goalw "Pair_neq_fst" ZF.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" thy [Pair_def] "<a,b>=b ==> P"
+qed_goalw "Pair_neq_snd" ZF.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" thy [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
- (fn _ => [ Fast_tac 1 ]);
+qed_goalw "Sigma_iff" ZF.thy [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
+ (fn _ => [ Blast_tac 1 ]);
 
 Addsimps [Sigma_iff];
 
-qed_goal "SigmaI" thy
+qed_goal "SigmaI" ZF.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" thy [Sigma_def]
+qed_goalw "SigmaE" ZF.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" thy
+qed_goal "SigmaE2" ZF.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" thy [Sigma_def]
+qed_goalw "Sigma_cong" ZF.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,32 +98,32 @@
 AddSIs [SigmaI];
 AddSEs [SigmaE2, SigmaE];
 
-qed_goal "Sigma_empty1" thy "Sigma(0,B) = 0"
- (fn _ => [ (Fast_tac 1) ]);
+qed_goal "Sigma_empty1" ZF.thy "Sigma(0,B) = 0"
+ (fn _ => [ (Blast_tac 1) ]);
 
-qed_goal "Sigma_empty2" thy "A*0 = 0"
- (fn _ => [ (Fast_tac 1) ]);
+qed_goal "Sigma_empty2" ZF.thy "A*0 = 0"
+ (fn _ => [ (Blast_tac 1) ]);
 
 Addsimps [Sigma_empty1, Sigma_empty2];
 
 
 (*** Projections: fst, snd ***)
 
-qed_goalw "fst_conv" thy [fst_def] "fst(<a,b>) = a"
- (fn _=> [ (fast_tac (!claset addIs [the_equality]) 1) ]);
+qed_goalw "fst_conv" ZF.thy [fst_def] "fst(<a,b>) = a"
+ (fn _=> [ (blast_tac (!claset addIs [the_equality]) 1) ]);
 
-qed_goalw "snd_conv" thy [snd_def] "snd(<a,b>) = b"
- (fn _=> [ (fast_tac (!claset addIs [the_equality]) 1) ]);
+qed_goalw "snd_conv" ZF.thy [snd_def] "snd(<a,b>) = b"
+ (fn _=> [ (blast_tac (!claset addIs [the_equality]) 1) ]);
 
 Addsimps [fst_conv,snd_conv];
 
-qed_goal "fst_type" thy "!!p. p:Sigma(A,B) ==> fst(p) : A"
+qed_goal "fst_type" ZF.thy "!!p. p:Sigma(A,B) ==> fst(p) : A"
  (fn _=> [ Auto_tac() ]);
 
-qed_goal "snd_type" thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))"
+qed_goal "snd_type" ZF.thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))"
  (fn _=> [ Auto_tac() ]);
 
-qed_goal "Pair_fst_snd_eq" thy
+qed_goal "Pair_fst_snd_eq" ZF.thy
     "!!a A B. a: Sigma(A,B) ==> <fst(a),snd(a)> = a"
  (fn _=> [ Auto_tac() ]);
 
@@ -131,13 +131,13 @@
 (*** Eliminator - split ***)
 
 (*A META-equality, so that it applies to higher types as well...*)
-qed_goalw "split" thy [split_def] "split(%x y.c(x,y), <a,b>) == c(a,b)"
+qed_goalw "split" ZF.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" thy
+qed_goal "split_type" ZF.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)"
@@ -145,7 +145,7 @@
   [ (rtac (major RS SigmaE) 1),
     (asm_simp_tac (!simpset addsimps prems) 1) ]);
 
-goalw thy [split_def]
+goalw ZF.thy [split_def]
   "!!u. u: A*B ==>   \
 \       R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))";
 by (Auto_tac());
@@ -154,11 +154,11 @@
 
 (*** split for predicates: result type o ***)
 
-goalw thy [split_def] "!!R a b. R(a,b) ==> split(R, <a,b>)";
+goalw ZF.thy [split_def] "!!R a b. R(a,b) ==> split(R, <a,b>)";
 by (Asm_simp_tac 1);
 qed "splitI";
 
-val major::sigma::prems = goalw thy [split_def]
+val major::sigma::prems = goalw ZF.thy [split_def]
     "[| split(R,z);  z:Sigma(A,B);                      \
 \       !!x y. [| z = <x,y>;  R(x,y) |] ==> P           \
 \    |] ==> P";
@@ -168,7 +168,7 @@
 by (Asm_full_simp_tac 1);
 qed "splitE";
 
-goalw thy [split_def] "!!R a b. split(R,<a,b>) ==> R(a,b)";
+goalw ZF.thy [split_def] "!!R a b. split(R,<a,b>) ==> R(a,b)";
 by (Full_simp_tac 1);
 qed "splitD";
 
diff -r 02c12d4c8b97 -r 6476784dba1c src/ZF/subset.ML
--- a/src/ZF/subset.ML	Wed Apr 02 15:37:35 1997 +0200
+++ b/src/ZF/subset.ML	Wed Apr 02 15:39:44 1997 +0200
@@ -9,38 +9,38 @@
 
 (*** cons ***)
 
-qed_goal "cons_subsetI" thy "!!a. [| a:C; B<=C |] ==> cons(a,B) <= C"
- (fn _ => [ Fast_tac 1 ]);
+qed_goal "cons_subsetI" ZF.thy "!!a. [| a:C; B<=C |] ==> cons(a,B) <= C"
+ (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "subset_consI" thy "B <= cons(a,B)"
- (fn _ => [ Fast_tac 1 ]);
+qed_goal "subset_consI" ZF.thy "B <= cons(a,B)"
+ (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "cons_subset_iff" thy "cons(a,B)<=C <-> a:C & B<=C"
- (fn _ => [ Fast_tac 1 ]);
+qed_goal "cons_subset_iff" ZF.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" thy "A<=0 <-> A=0"
- (fn _=> [ (Fast_tac 1) ]);
+qed_goal "subset_empty_iff" ZF.thy "A<=0 <-> A=0"
+ (fn _=> [ (Blast_tac 1) ]);
 
-qed_goal "subset_cons_iff" thy
+qed_goal "subset_cons_iff" ZF.thy
     "C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)"
- (fn _=> [ (Fast_tac 1) ]);
+ (fn _=> [ (Blast_tac 1) ]);
 
 (*** succ ***)
 
-qed_goal "subset_succI" thy "i <= succ(i)"
- (fn _=> [ (Fast_tac 1) ]);
+qed_goal "subset_succI" ZF.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" thy [succ_def]
+qed_goalw "succ_subsetI" ZF.thy [succ_def]
     "!!i j. [| i:j;  i<=j |] ==> succ(i)<=j"
- (fn _=> [ (Fast_tac 1) ]);
+ (fn _=> [ (Blast_tac 1) ]);
 
-qed_goalw "succ_subsetE" thy [succ_def] 
+qed_goalw "succ_subsetE" ZF.thy [succ_def] 
     "[| succ(i) <= j;  [| i:j;  i<=j |] ==> P \
 \    |] ==> P"
  (fn major::prems=>
@@ -49,22 +49,22 @@
 
 (*** singletons ***)
 
-qed_goal "singleton_subsetI" thy "!!a c. a:C ==> {a} <= C"
- (fn _=> [ (Fast_tac 1) ]);
+qed_goal "singleton_subsetI" ZF.thy "!!a c. a:C ==> {a} <= C"
+ (fn _=> [ (Blast_tac 1) ]);
 
-qed_goal "singleton_subsetD" thy "!!a C. {a} <= C  ==>  a:C"
- (fn _=> [ (Fast_tac 1) ]);
+qed_goal "singleton_subsetD" ZF.thy "!!a C. {a} <= C  ==>  a:C"
+ (fn _=> [ (Blast_tac 1) ]);
 
 (*** Big Union -- least upper bound of a set  ***)
 
-qed_goal "Union_subset_iff" thy "Union(A) <= C <-> (ALL x:A. x <= C)"
- (fn _ => [ Fast_tac 1 ]);
+qed_goal "Union_subset_iff" ZF.thy "Union(A) <= C <-> (ALL x:A. x <= C)"
+ (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Union_upper" thy
+qed_goal "Union_upper" ZF.thy
     "!!B A. B:A ==> B <= Union(A)"
- (fn _ => [ Fast_tac 1 ]);
+ (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Union_least" thy
+qed_goal "Union_least" ZF.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 thy "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))";
-by (fast_tac (!claset addSEs [equalityE]) 1);
+goal ZF.thy "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" thy
+qed_goal "UN_subset_iff" ZF.thy
      "(UN x:A.B(x)) <= C <-> (ALL x:A. B(x) <= C)"
- (fn _ => [ Fast_tac 1 ]);
+ (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "UN_upper" thy
+qed_goal "UN_upper" ZF.thy
     "!!x A. x:A ==> B(x) <= (UN x:A.B(x))"
  (fn _ => [ etac (RepFunI RS Union_upper) 1 ]);
 
-qed_goal "UN_least" thy
+qed_goal "UN_least" ZF.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" thy
+qed_goal "Inter_subset_iff" ZF.thy
      "!!a A. a: A  ==>  C <= Inter(A) <-> (ALL x:A. C <= x)"
- (fn _ => [ Fast_tac 1 ]);
+ (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Inter_lower" thy "!!B A. B:A ==> Inter(A) <= B"
- (fn _ => [ Fast_tac 1 ]);
+qed_goal "Inter_lower" ZF.thy "!!B A. B:A ==> Inter(A) <= B"
+ (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Inter_greatest" thy
+qed_goal "Inter_greatest" ZF.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" thy
+qed_goal "INT_lower" ZF.thy
     "!!x. x:A ==> (INT x:A.B(x)) <= B(x)"
- (fn _ => [ Fast_tac 1 ]);
+ (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "INT_greatest" thy
+qed_goal "INT_greatest" ZF.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,54 +121,54 @@
 
 (*** Finite Union -- the least upper bound of 2 sets ***)
 
-qed_goal "Un_subset_iff" thy "A Un B <= C <-> A <= C & B <= C"
- (fn _ => [ Fast_tac 1 ]);
+qed_goal "Un_subset_iff" ZF.thy "A Un B <= C <-> A <= C & B <= C"
+ (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Un_upper1" thy "A <= A Un B"
- (fn _ => [ Fast_tac 1 ]);
+qed_goal "Un_upper1" ZF.thy "A <= A Un B"
+ (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Un_upper2" thy "B <= A Un B"
- (fn _ => [ Fast_tac 1 ]);
+qed_goal "Un_upper2" ZF.thy "B <= A Un B"
+ (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Un_least" thy "!!A B C. [| A<=C;  B<=C |] ==> A Un B <= C"
- (fn _ => [ Fast_tac 1 ]);
+qed_goal "Un_least" ZF.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" thy "C <= A Int B <-> C <= A & C <= B"
- (fn _ => [ Fast_tac 1 ]);
+qed_goal "Int_subset_iff" ZF.thy "C <= A Int B <-> C <= A & C <= B"
+ (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Int_lower1" thy "A Int B <= A"
- (fn _ => [ Fast_tac 1 ]);
+qed_goal "Int_lower1" ZF.thy "A Int B <= A"
+ (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Int_lower2" thy "A Int B <= B"
- (fn _ => [ Fast_tac 1 ]);
+qed_goal "Int_lower2" ZF.thy "A Int B <= B"
+ (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Int_greatest" thy "!!A B C. [| C<=A;  C<=B |] ==> C <= A Int B"
- (fn _ => [ Fast_tac 1 ]);
+qed_goal "Int_greatest" ZF.thy "!!A B C. [| C<=A;  C<=B |] ==> C <= A Int B"
+ (fn _ => [ Blast_tac 1 ]);
 
 
 (*** Set difference *)
 
-qed_goal "Diff_subset" thy "A-B <= A"
- (fn _ => [ Fast_tac 1 ]);
+qed_goal "Diff_subset" ZF.thy "A-B <= A"
+ (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Diff_contains" thy
+qed_goal "Diff_contains" ZF.thy
     "!!C. [| C<=A;  C Int B = 0 |] ==> C <= A-B"
- (fn _ => [ (fast_tac (!claset addSEs [equalityE]) 1) ]);
+ (fn _ => [ (blast_tac (!claset addSEs [equalityE]) 1) ]);
 
 
 (** Collect **)
 
-qed_goal "Collect_subset" thy "Collect(A,P) <= A"
- (fn _ => [ Fast_tac 1 ]);
+qed_goal "Collect_subset" ZF.thy "Collect(A,P) <= A"
+ (fn _ => [ Blast_tac 1 ]);
 
 
 (** RepFun **)
 
-val prems = goal thy "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B";
-by (fast_tac (!claset addIs prems) 1);
+val prems = goal ZF.thy "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B";
+by (blast_tac (!claset addIs prems) 1);
 qed "RepFun_subset";
 
 val subset_SIs =
diff -r 02c12d4c8b97 -r 6476784dba1c src/ZF/upair.ML
--- a/src/ZF/upair.ML	Wed Apr 02 15:37:35 1997 +0200
+++ b/src/ZF/upair.ML	Wed Apr 02 15:39:44 1997 +0200
@@ -21,49 +21,48 @@
 
 (*** Unordered pairs - Upair ***)
 
-qed_goalw "Upair_iff" thy [Upair_def]
+qed_goalw "Upair_iff" ZF.thy [Upair_def]
     "c : Upair(a,b) <-> (c=a | c=b)"
- (fn _ => [ (fast_tac (!claset addEs [Pow_neq_0, sym RS Pow_neq_0]) 1) ]);
+ (fn _ => [ (blast_tac (!claset addEs [Pow_neq_0, sym RS Pow_neq_0]) 1) ]);
 
 Addsimps [Upair_iff];
 
-qed_goal "UpairI1" thy "a : Upair(a,b)"
+qed_goal "UpairI1" ZF.thy "a : Upair(a,b)"
  (fn _ => [ Simp_tac 1 ]);
 
-qed_goal "UpairI2" thy "b : Upair(a,b)"
+qed_goal "UpairI2" ZF.thy "b : Upair(a,b)"
  (fn _ => [ Simp_tac 1 ]);
 
-qed_goal "UpairE" thy
+qed_goal "UpairE" ZF.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),
     (REPEAT (eresolve_tac prems 1)) ]);
 
-(*UpairI1/2 should become UpairCI?*)
 AddSIs [UpairI1,UpairI2];
 AddSEs [UpairE];
 
 (*** Rules for binary union -- Un -- defined via Upair ***)
 
-qed_goalw "Un_iff" thy [Un_def] "c : A Un B <-> (c:A | c:B)"
- (fn _ => [ Fast_tac 1 ]);
+qed_goalw "Un_iff" ZF.thy [Un_def] "c : A Un B <-> (c:A | c:B)"
+ (fn _ => [ Blast_tac 1 ]);
 
 Addsimps [Un_iff];
 
-qed_goal "UnI1" thy "!!c. c : A ==> c : A Un B"
+qed_goal "UnI1" ZF.thy "!!c. c : A ==> c : A Un B"
  (fn _ => [ Asm_simp_tac 1 ]);
 
-qed_goal "UnI2" thy "!!c. c : B ==> c : A Un B"
+qed_goal "UnI2" ZF.thy "!!c. c : B ==> c : A Un B"
  (fn _ => [ Asm_simp_tac 1 ]);
 
-qed_goal "UnE" thy 
+qed_goal "UnE" ZF.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'" thy
+qed_goal "UnE'" ZF.thy
     "[| c : A Un B;  c:A ==> P;  [| c:B;  c~:A |] ==> P |] ==> P"
  (fn major::prems =>
   [(rtac (major RS UnE) 1),
@@ -74,9 +73,9 @@
    (etac notnotD 1)]);
 
 (*Classical introduction rule: no commitment to A vs B*)
-qed_goal "UnCI" thy "(c ~: B ==> c : A) ==> c : A Un B"
+qed_goal "UnCI" ZF.thy "(c ~: B ==> c : A) ==> c : A Un B"
  (fn prems=>
-  [ Simp_tac 1, fast_tac (!claset addSIs prems) 1 ]);
+  [ Simp_tac 1, blast_tac (!claset addSIs prems) 1 ]);
 
 AddSIs [UnCI];
 AddSEs [UnE];
@@ -84,21 +83,21 @@
 
 (*** Rules for small intersection -- Int -- defined via Upair ***)
 
-qed_goalw "Int_iff" thy [Int_def] "c : A Int B <-> (c:A & c:B)"
- (fn _ => [ Fast_tac 1 ]);
+qed_goalw "Int_iff" ZF.thy [Int_def] "c : A Int B <-> (c:A & c:B)"
+ (fn _ => [ Blast_tac 1 ]);
 
 Addsimps [Int_iff];
 
-qed_goal "IntI" thy "!!c. [| c : A;  c : B |] ==> c : A Int B"
+qed_goal "IntI" ZF.thy "!!c. [| c : A;  c : B |] ==> c : A Int B"
  (fn _ => [ Asm_simp_tac 1 ]);
 
-qed_goal "IntD1" thy "!!c. c : A Int B ==> c : A"
+qed_goal "IntD1" ZF.thy "!!c. c : A Int B ==> c : A"
  (fn _ => [ Asm_full_simp_tac 1 ]);
 
-qed_goal "IntD2" thy "!!c. c : A Int B ==> c : B"
+qed_goal "IntD2" ZF.thy "!!c. c : A Int B ==> c : B"
  (fn _ => [ Asm_full_simp_tac 1 ]);
 
-qed_goal "IntE" thy
+qed_goal "IntE" ZF.thy
     "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P"
  (fn prems=>
   [ (resolve_tac prems 1),
@@ -109,21 +108,21 @@
 
 (*** Rules for set difference -- defined via Upair ***)
 
-qed_goalw "Diff_iff" thy [Diff_def] "c : A-B <-> (c:A & c~:B)"
- (fn _ => [ Fast_tac 1 ]);
+qed_goalw "Diff_iff" ZF.thy [Diff_def] "c : A-B <-> (c:A & c~:B)"
+ (fn _ => [ Blast_tac 1 ]);
 
 Addsimps [Diff_iff];
 
-qed_goal "DiffI" thy "!!c. [| c : A;  c ~: B |] ==> c : A - B"
+qed_goal "DiffI" ZF.thy "!!c. [| c : A;  c ~: B |] ==> c : A - B"
  (fn _ => [ Asm_simp_tac 1 ]);
 
-qed_goal "DiffD1" thy "!!c. c : A - B ==> c : A"
+qed_goal "DiffD1" ZF.thy "!!c. c : A - B ==> c : A"
  (fn _ => [ Asm_full_simp_tac 1 ]);
 
-qed_goal "DiffD2" thy "!!c. c : A - B ==> c ~: B"
+qed_goal "DiffD2" ZF.thy "!!c. c : A - B ==> c ~: B"
  (fn _ => [ Asm_full_simp_tac 1 ]);
 
-qed_goal "DiffE" thy
+qed_goal "DiffE" ZF.thy
     "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P"
  (fn prems=>
   [ (resolve_tac prems 1),
@@ -134,27 +133,27 @@
 
 (*** Rules for cons -- defined via Un and Upair ***)
 
-qed_goalw "cons_iff" thy [cons_def] "a : cons(b,A) <-> (a=b | a:A)"
- (fn _ => [ Fast_tac 1 ]);
+qed_goalw "cons_iff" ZF.thy [cons_def] "a : cons(b,A) <-> (a=b | a:A)"
+ (fn _ => [ Blast_tac 1 ]);
 
 Addsimps [cons_iff];
 
-qed_goal "consI1" thy "a : cons(a,B)"
+qed_goal "consI1" ZF.thy "a : cons(a,B)"
  (fn _ => [ Simp_tac 1 ]);
 
 Addsimps [consI1];
 
-qed_goal "consI2" thy "!!B. a : B ==> a : cons(b,B)"
+qed_goal "consI2" ZF.thy "!!B. a : B ==> a : cons(b,B)"
  (fn _ => [ Asm_simp_tac 1 ]);
 
-qed_goal "consE" thy
+qed_goal "consE" ZF.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'" thy
+qed_goal "consE'" ZF.thy
     "[| a : cons(b,A);  a=b ==> P;  [| a:A;  a~=b |] ==> P |] ==> P"
  (fn major::prems =>
   [(rtac (major RS consE) 1),
@@ -165,15 +164,15 @@
    (etac notnotD 1)]);
 
 (*Classical introduction rule*)
-qed_goal "consCI" thy "(a~:B ==> a=b) ==> a: cons(b,B)"
+qed_goal "consCI" ZF.thy "(a~:B ==> a=b) ==> a: cons(b,B)"
  (fn prems=>
-  [ Simp_tac 1, fast_tac (!claset addSIs prems) 1 ]);
+  [ Simp_tac 1, blast_tac (!claset addSIs prems) 1 ]);
 
 AddSIs [consCI];
 AddSEs [consE];
 
-qed_goal "cons_not_0" thy "cons(a,B) ~= 0"
- (fn _ => [ (fast_tac (!claset addEs [equalityE]) 1) ]);
+qed_goal "cons_not_0" ZF.thy "cons(a,B) ~= 0"
+ (fn _ => [ (blast_tac (!claset addEs [equalityE]) 1) ]);
 
 bind_thm ("cons_neq_0", cons_not_0 RS notE);
 
@@ -182,10 +181,10 @@
 
 (*** Singletons - using cons ***)
 
-qed_goal "singleton_iff" thy "a : {b} <-> a=b"
+qed_goal "singleton_iff" ZF.thy "a : {b} <-> a=b"
  (fn _ => [ Simp_tac 1 ]);
 
-qed_goal "singletonI" thy "a : {a}"
+qed_goal "singletonI" ZF.thy "a : {a}"
  (fn _=> [ (rtac consI1 1) ]);
 
 bind_thm ("singletonE", make_elim (singleton_iff RS iffD1));
@@ -195,25 +194,25 @@
 
 (*** Rules for Descriptions ***)
 
-qed_goalw "the_equality" thy [the_def]
+qed_goalw "the_equality" ZF.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" thy
+qed_goal "the_equality2" ZF.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" thy "EX! x. P(x) ==> P(THE x. P(x))"
+qed_goal "theI" ZF.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" thy
+qed_goal "theI2" ZF.thy
     "[| EX! x. P(x);  !!x. P(x) ==> Q(x) |] ==> Q(THE x.P(x))"
  (fn prems => [ resolve_tac prems 1, 
                 rtac theI 1, 
@@ -223,49 +222,49 @@
   (THE x.P(x))  rewrites to  (THE x. Q(x))  *)
 
 (*If it's "undefined", it's zero!*)
-qed_goalw "the_0" thy [the_def]
+qed_goalw "the_0" ZF.thy [the_def]
     "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
- (fn _ => [ (fast_tac (!claset addSEs [ReplaceE]) 1) ]);
+ (fn _ => [ (deepen_tac (!claset addSEs [ReplaceE]) 0 1) ]);
 
 
 (*** if -- a conditional expression for formulae ***)
 
-goalw thy [if_def] "if(True,a,b) = a";
-by (fast_tac (!claset addIs [the_equality]) 1);
+goalw ZF.thy [if_def] "if(True,a,b) = a";
+by (blast_tac (!claset addSIs [the_equality]) 1);
 qed "if_true";
 
-goalw thy [if_def] "if(False,a,b) = b";
-by (fast_tac (!claset addIs [the_equality]) 1);
+goalw ZF.thy [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 thy [if_def]
+val prems = goalw ZF.thy [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 thy [if_def] "!!P. P ==> if(P,a,b) = a";
-by (fast_tac (!claset addSIs [the_equality]) 1);
+goalw ZF.thy [if_def] "!!P. 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 thy [if_def] "!!P. ~P ==> if(P,a,b) = b";
-by (fast_tac (!claset addSIs [the_equality]) 1);
+goalw ZF.thy [if_def] "!!P. ~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 "expand_if" thy
+qed_goal "expand_if" ZF.thy
     "P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))"
  (fn _=> [ (excluded_middle_tac "Q" 1),
            (Asm_simp_tac 1),
            (Asm_simp_tac 1) ]);
 
-qed_goal "if_iff" thy "a: if(P,x,y) <-> P & a:x | ~P & a:y"
+qed_goal "if_iff" ZF.thy "a: if(P,x,y) <-> P & a:x | ~P & a:y"
  (fn _=> [ (simp_tac (!simpset setloop split_tac [expand_if]) 1) ]);
 
-qed_goal "if_type" thy
+qed_goal "if_type" ZF.thy
     "[| P ==> a: A;  ~P ==> b: A |] ==> if(P,a,b): A"
  (fn prems=> [ (simp_tac 
                 (!simpset addsimps prems setloop split_tac [expand_if]) 1) ]);
@@ -274,47 +273,48 @@
 (*** Foundation lemmas ***)
 
 (*was called mem_anti_sym*)
-qed_goal "mem_asym" thy "!!P. [| a:b;  b:a |] ==> P"
- (fn _=>
-  [ (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1),
-    REPEAT (fast_tac (!claset addSEs [equalityE]) 1) ]);
+qed_goal "mem_asym" ZF.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" thy "a:a ==> P"
+qed_goal "mem_irrefl" ZF.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" thy "a ~: a"
+qed_goal "mem_not_refl" ZF.thy "a ~: a"
  (K [ (rtac notI 1), (etac mem_irrefl 1) ]);
 
 (*Good for proving inequalities by rewriting*)
-qed_goal "mem_imp_not_eq" thy "!!a A. a:A ==> a ~= A"
- (fn _=> [ fast_tac (!claset addSEs [mem_irrefl]) 1 ]);
+qed_goal "mem_imp_not_eq" ZF.thy "!!a A. a:A ==> a ~= A"
+ (fn _=> [ blast_tac (!claset addSEs [mem_irrefl]) 1 ]);
 
 (*** Rules for succ ***)
 
-qed_goalw "succ_iff" thy [succ_def] "i : succ(j) <-> i=j | i:j"
- (fn _ => [ Fast_tac 1 ]);
+qed_goalw "succ_iff" ZF.thy [succ_def] "i : succ(j) <-> i=j | i:j"
+ (fn _ => [ Blast_tac 1 ]);
 
-qed_goalw "succI1" thy [succ_def] "i : succ(i)"
+qed_goalw "succI1" ZF.thy [succ_def] "i : succ(i)"
  (fn _=> [ (rtac consI1 1) ]);
 
 Addsimps [succI1];
 
-qed_goalw "succI2" thy [succ_def]
+qed_goalw "succI2" ZF.thy [succ_def]
     "i : j ==> i : succ(j)"
  (fn [prem]=> [ (rtac (prem RS consI2) 1) ]);
 
-qed_goalw "succE" thy [succ_def]
+qed_goalw "succE" ZF.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" thy "(i~:j ==> i=j) ==> i: succ(j)"
+qed_goal "succCI" ZF.thy "(i~:j ==> i=j) ==> i: succ(j)"
  (fn [prem]=>
   [ (rtac (disjCI RS (succ_iff RS iffD2)) 1),
     (etac prem 1) ]);
@@ -322,8 +322,8 @@
 AddSIs [succCI];
 AddSEs [succE];
 
-qed_goal "succ_not_0" thy "succ(n) ~= 0"
- (fn _=> [ (fast_tac (!claset addSEs [equalityE]) 1) ]);
+qed_goal "succ_not_0" ZF.thy "succ(n) ~= 0"
+ (fn _=> [ (blast_tac (!claset addSEs [equalityE]) 1) ]);
 
 bind_thm ("succ_neq_0", succ_not_0 RS notE);
 
@@ -338,13 +338,15 @@
 bind_thm ("succ_neq_self", succI1 RS mem_imp_not_eq RS not_sym);
 
 
-qed_goal "succ_inject_iff" thy "succ(m) = succ(n) <-> m=n"
- (fn _=> [ (fast_tac (!claset addEs [mem_asym, equalityE]) 1) ]);
+qed_goal "succ_inject_iff" ZF.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);
 
 Addsimps [succ_inject_iff];
 AddSDs [succ_inject];
 
+(*Not needed now that cons is available.  Deletion reduces the search space.*)
+Delrules [UpairI1,UpairI2,UpairE];
 
 use"simpdata.ML";