src/ZF/Sum.thy
changeset 5325 f7a5e06adea1
parent 3940 1d5bee4d047f
child 13220 62c899c77151
     1.1 --- a/src/ZF/Sum.thy	Mon Aug 17 13:06:29 1998 +0200
     1.2 +++ b/src/ZF/Sum.thy	Mon Aug 17 13:09:08 1998 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  "Part" primitive for simultaneous recursive type definitions
     1.5  *)
     1.6  
     1.7 -Sum = Bool + pair + 
     1.8 +Sum = Bool + equalities + 
     1.9  
    1.10  global
    1.11