--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Fixedpt.thy Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,23 @@
+(* Title: ZF/fixedpt.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1992 University of Cambridge
+
+Least and greatest fixed points
+*)
+
+Fixedpt = ZF +
+consts
+ bnd_mono :: "[i,i=>i]=>o"
+ lfp, gfp :: "[i,i=>i]=>i"
+
+rules
+ (*monotone operator from Pow(D) to itself*)
+ bnd_mono_def
+ "bnd_mono(D,h) == h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))"
+
+ lfp_def "lfp(D,h) == Inter({X: Pow(D). h(X) <= X})"
+
+ gfp_def "gfp(D,h) == Union({X: Pow(D). X <= h(X)})"
+
+end