src/ZF/Fixedpt.thy
changeset 6093 87bf8c03b169
parent 3940 1d5bee4d047f
child 13168 afcbca3498b0
     1.1 --- a/src/ZF/Fixedpt.thy	Tue Jan 12 13:54:51 1999 +0100
     1.2 +++ b/src/ZF/Fixedpt.thy	Tue Jan 12 15:17:37 1999 +0100
     1.3 @@ -8,14 +8,10 @@
     1.4  
     1.5  Fixedpt = domrange +
     1.6  
     1.7 -global
     1.8 -
     1.9  consts
    1.10    bnd_mono    :: [i,i=>i]=>o
    1.11    lfp, gfp    :: [i,i=>i]=>i
    1.12  
    1.13 -local
    1.14 -
    1.15  defs
    1.16    (*monotone operator from Pow(D) to itself*)
    1.17    bnd_mono_def