--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/Hartog.thy	Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,18 @@
+(*  Title: 	ZF/AC/Hartog.thy
+    ID:         $Id$
+    Author: 	Krzysztof Gr`abczewski
+
+Hartog's function.
+*)
+
+Hartog = Cardinal +
+
+consts
+
+  Hartog :: "i => i"
+
+defs
+
+  Hartog_def "Hartog(X) == LEAST i. ~i lepoll X"
+
+end
\ No newline at end of file