--- a/src/ZF/AC/AC2_AC6.ML Tue Mar 04 10:41:33 1997 +0100
+++ b/src/ZF/AC/AC2_AC6.ML Tue Mar 04 10:42:28 1997 +0100
@@ -78,7 +78,7 @@
goalw thy AC_defs "!!Z. AC1 ==> AC4";
by (REPEAT (resolve_tac [allI, impI] 1));
by (REPEAT (eresolve_tac [allE, lemma RSN (2, impE), exE] 1));
-by (fast_tac (!claset addSIs [lam_type] addSEs [apply_type]) 1);
+by (best_tac (!claset addSIs [lam_type] addSEs [apply_type]) 1);
qed "AC1_AC4";
--- a/src/ZF/Ordinal.ML Tue Mar 04 10:41:33 1997 +0100
+++ b/src/ZF/Ordinal.ML Tue Mar 04 10:42:28 1997 +0100
@@ -87,7 +87,7 @@
(*** Natural Deduction rules for Ord ***)
val prems = goalw Ordinal.thy [Ord_def]
- "[| Transset(i); !!x. x:i ==> Transset(x) |] ==> Ord(i) ";
+ "[| Transset(i); !!x. x:i ==> Transset(x) |] ==> Ord(i)";
by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
qed "OrdI";
@@ -623,7 +623,7 @@
qed "le_implies_UN_le_UN";
goal Ordinal.thy "!!i. Ord(i) ==> (UN y:i. succ(y)) = i";
-by (fast_tac (!claset addEs [Ord_trans]) 1);
+by (best_tac (!claset addEs [Ord_trans]) 1);
qed "Ord_equality";
(*Holds for all transitive sets, not just ordinals*)