--- a/src/ZF/Cardinal.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/ZF/Cardinal.thy Tue Aug 27 11:03:05 2002 +0200
@@ -892,7 +892,7 @@
done
(* Induction principle for Finite(A), by Sidi Ehmety *)
-lemma Finite_induct:
+lemma Finite_induct [case_names 0 cons, induct set: Finite]:
"[| Finite(A); P(0);
!! x B. [| Finite(B); x ~: B; P(B) |] ==> P(cons(x, B)) |]
==> P(A)"
@@ -900,8 +900,6 @@
apply (blast intro: Fin_into_Finite)+
done
-lemmas Finite_induct = Finite_induct [case_names 0 cons, induct set: Finite]
-
(*Sidi Ehmety. The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *)
lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)"
apply (unfold Finite_def)