src/ZF/Finite.thy
changeset 32960 69916a850301
parent 26056 6a0801279f4c
child 45602 2a858377c3d2
     1.1 --- a/src/ZF/Finite.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/ZF/Finite.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      ZF/Finite.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   1994  University of Cambridge
     1.8  
     1.9 @@ -13,8 +12,8 @@
    1.10  (*The natural numbers as a datatype*)
    1.11  rep_datatype
    1.12    elimination    natE
    1.13 -  induction	 nat_induct
    1.14 -  case_eqns	 nat_case_0 nat_case_succ
    1.15 +  induction      nat_induct
    1.16 +  case_eqns      nat_case_0 nat_case_succ
    1.17    recursor_eqns  recursor_0 recursor_succ
    1.18  
    1.19