src/ZF/Sum.thy

     "+"         :: [i,i]=>i                     (infixr 65)
     Inl,Inr     :: i=>i
     case        :: [i=>i, i=>i, i]=>i
     Part        :: [i,i=>i] => i
 
-path Sum
+local
 
 defs
     sum_def     "A+B == {0}*A Un {1}*B"
     Inl_def     "Inl(a) == <0,a>"
     Inr_def     "Inr(b) == <1,b>"