src/ZF/Finite.thy
changeset 13524 604d0f3622d6
parent 13356 c9cfe1638bf2
child 13615 449a70d88b38
     1.1 --- a/src/ZF/Finite.thy	Tue Aug 27 11:03:02 2002 +0200
     1.2 +++ b/src/ZF/Finite.thy	Tue Aug 27 11:03:05 2002 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4  (** Induction on finite sets **)
     1.5  
     1.6  (*Discharging x~:y entails extra work*)
     1.7 -lemma Fin_induct:
     1.8 +lemma Fin_induct [case_names 0 cons, induct set: Fin]:
     1.9      "[| b: Fin(A);
    1.10          P(0);
    1.11          !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y))
    1.12 @@ -67,9 +67,6 @@
    1.13  apply simp
    1.14  done
    1.15  
    1.16 -(*fixed up for induct method*)
    1.17 -lemmas Fin_induct = Fin_induct [case_names 0 cons, induct set: Fin]
    1.18 -
    1.19  
    1.20  (** Simplification for Fin **)
    1.21  declare Fin.intros [simp]