changeset 1401 | 0c439768f45c |
parent 753 | ec86863e87c8 |
child 1478 | 2b8c2a7547ab |
--- a/src/ZF/Fixedpt.thy Fri Dec 08 19:48:15 1995 +0100 +++ b/src/ZF/Fixedpt.thy Sat Dec 09 13:36:11 1995 +0100 @@ -8,8 +8,8 @@ Fixedpt = ZF + "domrange" + consts - bnd_mono :: "[i,i=>i]=>o" - lfp, gfp :: "[i,i=>i]=>i" + bnd_mono :: [i,i=>i]=>o + lfp, gfp :: [i,i=>i]=>i defs (*monotone operator from Pow(D) to itself*)