src/ZF/Finite.thy
changeset 13328 703de709a64b
parent 13269 3ba9be497c33
child 13356 c9cfe1638bf2
     1.1 --- a/src/ZF/Finite.thy	Tue Jul 09 23:03:21 2002 +0200
     1.2 +++ b/src/ZF/Finite.thy	Tue Jul 09 23:05:26 2002 +0200
     1.3 @@ -3,13 +3,13 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1994  University of Cambridge
     1.6  
     1.7 -Finite powerset operator; finite function space
     1.8 -
     1.9  prove X:Fin(A) ==> |X| < nat
    1.10  
    1.11  prove:  b: Fin(A) ==> inj(b,b) <= surj(b,b)
    1.12  *)
    1.13  
    1.14 +header{*Finite Powerset Operator and Finite Function Space*}
    1.15 +
    1.16  theory Finite = Inductive + Epsilon + Nat:
    1.17  
    1.18  (*The natural numbers as a datatype*)