--- a/src/ZF/Finite.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Finite.ML Thu Jan 07 18:30:55 1999 +0100
@@ -10,8 +10,6 @@
prove: b: Fin(A) ==> inj(b,b)<=surj(b,b)
*)
-open Finite;
-
(*** Finite powerset operator ***)
Goalw Fin.defs "A<=B ==> Fin(A) <= Fin(B)";
@@ -104,7 +102,7 @@
(*Functions from a finite ordinal*)
Goal "n: nat ==> n->A <= Fin(nat*A)";
-by (nat_ind_tac "n" [] 1);
+by (induct_tac "n" 1);
by (simp_tac (simpset() addsimps [Pi_empty1, subset_iff, cons_iff]) 1);
by (asm_simp_tac
(simpset() addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);