--- a/src/ZF/Finite.thy Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Finite.thy Tue Jul 09 23:05:26 2002 +0200
@@ -3,13 +3,13 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-Finite powerset operator; finite function space
-
prove X:Fin(A) ==> |X| < nat
prove: b: Fin(A) ==> inj(b,b) <= surj(b,b)
*)
+header{*Finite Powerset Operator and Finite Function Space*}
+
theory Finite = Inductive + Epsilon + Nat:
(*The natural numbers as a datatype*)