src/ZF/Finite.thy
changeset 13524 604d0f3622d6
parent 13356 c9cfe1638bf2
child 13615 449a70d88b38
--- a/src/ZF/Finite.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/ZF/Finite.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -56,7 +56,7 @@
 (** Induction on finite sets **)
 
 (*Discharging x~:y entails extra work*)
-lemma Fin_induct:
+lemma Fin_induct [case_names 0 cons, induct set: Fin]:
     "[| b: Fin(A);
         P(0);
         !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y))
@@ -67,9 +67,6 @@
 apply simp
 done
 
-(*fixed up for induct method*)
-lemmas Fin_induct = Fin_induct [case_names 0 cons, induct set: Fin]
-
 
 (** Simplification for Fin **)
 declare Fin.intros [simp]