src/ZF/Fixedpt.thy
changeset 13168 afcbca3498b0
parent 6093 87bf8c03b169
child 13218 3732064ccbd1
--- 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