src/ZF/AC/AC2_AC6.ML
changeset 2717 b29c45ef3d86
parent 2496 40efb87985b5
child 4091 771b1f6422a8
--- 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";