--- a/src/ZF/Sum.thy Mon Aug 17 13:06:29 1998 +0200 +++ b/src/ZF/Sum.thy Mon Aug 17 13:09:08 1998 +0200 @@ -7,7 +7,7 @@ "Part" primitive for simultaneous recursive type definitions *) -Sum = Bool + pair + +Sum = Bool + equalities + global