--- a/src/ZF/Resid/Redex.thy Wed Apr 02 15:29:48 1997 +0200 +++ b/src/ZF/Resid/Redex.thy Wed Apr 02 15:30:44 1997 +0200 @@ -5,7 +5,7 @@ Logic Image: ZF *) -Redex = Univ + +Redex = Datatype + consts redexes :: i