src/ZF/Sum.thy
changeset 3940 1d5bee4d047f
parent 3923 c257b82a1200
child 5325 f7a5e06adea1
     1.1 --- a/src/ZF/Sum.thy	Mon Oct 20 10:53:25 1997 +0200
     1.2 +++ b/src/ZF/Sum.thy	Mon Oct 20 10:53:42 1997 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4      case        :: [i=>i, i=>i, i]=>i
     1.5      Part        :: [i,i=>i] => i
     1.6  
     1.7 -path Sum
     1.8 +local
     1.9  
    1.10  defs
    1.11      sum_def     "A+B == {0}*A Un {1}*B"