src/ZF/Sum.thy
changeset 2469 b50b8c0eec01
parent 1478 2b8c2a7547ab
child 3923 c257b82a1200
     1.1 --- a/src/ZF/Sum.thy	Fri Jan 03 10:48:28 1997 +0100
     1.2 +++ b/src/ZF/Sum.thy	Fri Jan 03 15:01:55 1997 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  "Part" primitive for simultaneous recursive type definitions
     1.5  *)
     1.6  
     1.7 -Sum = Bool + "simpdata" +
     1.8 +Sum = Bool + pair + 
     1.9  consts
    1.10      "+"         :: [i,i]=>i                     (infixr 65)
    1.11      Inl,Inr     :: i=>i