--- a/src/ZF/AC/AC_Equiv.ML Thu Jan 13 17:30:23 2000 +0100
+++ b/src/ZF/AC/AC_Equiv.ML Thu Jan 13 17:31:30 2000 +0100
@@ -4,9 +4,6 @@
*)
-
-open AC_Equiv;
-
val WO_defs = [WO1_def, WO2_def, WO3_def, WO4_def, WO5_def, WO6_def, WO8_def];
val AC_defs = [AC0_def, AC1_def, AC2_def, AC3_def, AC4_def, AC5_def,
@@ -99,10 +96,6 @@
addSIs [major RS CollectD1 RS Pi_type, major RS CollectD2]) 1);
qed "inj_strengthen_type";
-Goalw [Finite_def] "n:nat ==> Finite(n)";
-by (fast_tac (claset() addSIs [eqpoll_refl]) 1);
-qed "nat_into_Finite";
-
Goalw [Finite_def] "~Finite(nat)";
by (fast_tac (claset() addSDs [eqpoll_imp_lepoll]
addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1);