--- a/src/ZF/Resid/Redex.thy Fri Jul 14 13:39:03 2000 +0200 +++ b/src/ZF/Resid/Redex.thy Fri Jul 14 13:57:00 2000 +0200 @@ -5,7 +5,7 @@ Logic Image: ZF *) -Redex = Datatype + +Redex = Main + consts redexes :: i