A few more standard simprules, TCs, etc.

--- a/src/ZF/QPair.ML	Tue Jan 22 21:19:15 2002 +0100
+++ b/src/ZF/QPair.ML	Wed Jan 23 11:43:53 2002 +0100
@@ -110,10 +110,12 @@
 Goal "p:QSigma(A,B) ==> qfst(p) : A";
 by (Auto_tac) ;
 qed "qfst_type";
+AddTCs [qfst_type];
 
 Goal "p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))";
 by (Auto_tac) ;
 qed "qsnd_type";
+AddTCs [qsnd_type];
 
 Goal "a: QSigma(A,B) ==> <qfst(a); qsnd(a)> = a";
 by Auto_tac;

--- a/src/ZF/ZF.ML	Tue Jan 22 21:19:15 2002 +0100
+++ b/src/ZF/ZF.ML	Wed Jan 23 11:43:53 2002 +0100
@@ -447,8 +447,7 @@
 by (etac (Pow_iff RS iffD1) 1) ;
 qed "PowD";
 
-AddSIs [PowI];
-AddSDs [PowD];
+AddIffs [Pow_iff];
 
 
 (*** Rules for the empty set ***)

--- a/src/ZF/Zorn.ML	Tue Jan 22 21:19:15 2002 +0100
+++ b/src/ZF/Zorn.ML	Wed Jan 23 11:43:53 2002 +0100
@@ -181,7 +181,7 @@
 by (rtac CollectI 1);
 by (rtac lam_type 1);
 by (Asm_simp_tac 1);
-by (fast_tac (claset() addSIs [super_subset_chain RS subsetD,
+by (blast_tac (claset() addDs [super_subset_chain RS subsetD,
 			       chain_subset_Pow RS subsetD,
 			       choice_super]) 1);
 (*Now, verify that it increases*)
@@ -202,7 +202,7 @@
 \      |] ==> c: chain(S)";
 by (etac TFin_induct 1);
 by (asm_simp_tac 
-    (simpset() addsimps [chain_subset_Pow RS subsetD, 
+    (simpset() addsimps [chain_subset_Pow RS subsetD RS PowD, 
 			 choice_super RS (super_subset_chain RS subsetD)]) 1);
 by (rewtac chain_def);
 by (rtac CollectI 1 THEN Blast_tac 1);
@@ -227,9 +227,9 @@
 by (rtac refl 2);
 by (asm_full_simp_tac 
     (simpset() addsimps [subset_refl RS TFin_UnionI RS
-			 (TFin.dom_subset RS subsetD)]) 1);
+			 (TFin.dom_subset RS subsetD RS PowD)]) 1);
 by (eresolve_tac [choice_not_equals RS notE] 1);
-by (REPEAT (assume_tac 1));
+by (REPEAT (assume_tac 1)); 
 qed "Hausdorff";
 
 

--- a/src/ZF/pair.ML	Tue Jan 22 21:19:15 2002 +0100
+++ b/src/ZF/pair.ML	Wed Jan 23 11:43:53 2002 +0100
@@ -134,10 +134,12 @@
 Goal "p:Sigma(A,B) ==> fst(p) : A";
 by (Auto_tac) ;
 qed "fst_type";
+AddTCs [fst_type];
 
 Goal "p:Sigma(A,B) ==> snd(p) : B(fst(p))";
 by (Auto_tac) ;
 qed "snd_type";
+AddTCs [snd_type];
 
 Goal "a: Sigma(A,B) ==> <fst(a),snd(a)> = a";
 by (Auto_tac) ;