src/ZF/Sum.thy
changeset 3923 c257b82a1200
parent 2469 b50b8c0eec01
child 3940 1d5bee4d047f
     1.1 --- a/src/ZF/Sum.thy	Fri Oct 17 17:39:04 1997 +0200
     1.2 +++ b/src/ZF/Sum.thy	Fri Oct 17 17:40:02 1997 +0200
     1.3 @@ -8,12 +8,17 @@
     1.4  *)
     1.5  
     1.6  Sum = Bool + pair + 
     1.7 +
     1.8 +global
     1.9 +
    1.10  consts
    1.11      "+"         :: [i,i]=>i                     (infixr 65)
    1.12      Inl,Inr     :: i=>i
    1.13      case        :: [i=>i, i=>i, i]=>i
    1.14      Part        :: [i,i=>i] => i
    1.15  
    1.16 +path Sum
    1.17 +
    1.18  defs
    1.19      sum_def     "A+B == {0}*A Un {1}*B"
    1.20      Inl_def     "Inl(a) == <0,a>"