src/ZF/Fixedpt.thy

--- a/src/ZF/Fixedpt.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Fixedpt.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -11,7 +11,7 @@
   bnd_mono    :: "[i,i=>i]=>o"
   lfp, gfp    :: "[i,i=>i]=>i"
 
-rules
+defs
   (*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))"