--- a/src/ZF/Fixedpt.thy Fri Oct 17 17:39:04 1997 +0200
+++ b/src/ZF/Fixedpt.thy Fri Oct 17 17:40:02 1997 +0200
@@ -7,10 +7,15 @@
*)
Fixedpt = domrange +
+
+global
+
consts
bnd_mono :: [i,i=>i]=>o
lfp, gfp :: [i,i=>i]=>i
+path Fixedpt
+
defs
(*monotone operator from Pow(D) to itself*)
bnd_mono_def