# HG changeset patch
# User paulson
# Date 857468548 -3600
# Node ID b29c45ef3d86c613585b593297bd0e34c2453ee2
# Parent  9e11a914156af260fd6c864162f9add74331f95e
best_tac avoids looping with change to RepFun_eqI in claset

diff -r 9e11a914156a -r b29c45ef3d86 src/ZF/AC/AC2_AC6.ML
--- 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";
 
 
diff -r 9e11a914156a -r b29c45ef3d86 src/ZF/Ordinal.ML
--- 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*)