--- a/src/ZF/Fixedpt.thy Mon May 20 12:59:59 2002 +0200 +++ b/src/ZF/Fixedpt.thy Tue May 21 13:06:36 2002 +0200 @@ -6,7 +6,7 @@ Least and greatest fixed points *) -Fixedpt = domrange + +Fixedpt = equalities + consts bnd_mono :: [i,i=>i]=>o