src/ZF/Sum.thy
changeset 1108 22b256c8c9fb
parent 753 ec86863e87c8
child 1401 0c439768f45c
     1.1 --- a/src/ZF/Sum.thy	Thu May 04 02:01:24 1995 +0200
     1.2 +++ b/src/ZF/Sum.thy	Thu May 04 02:01:49 1995 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4      sum_def     "A+B == {0}*A Un {1}*B"
     1.5      Inl_def     "Inl(a) == <0,a>"
     1.6      Inr_def     "Inr(b) == <1,b>"
     1.7 -    case_def    "case(c,d) == split(%y z. cond(y, d(z), c(z)))"
     1.8 +    case_def    "case(c,d) == (%<y,z>. cond(y, d(z), c(z)))"
     1.9  
    1.10    (*operator for selecting out the various summands*)
    1.11      Part_def	"Part(A,h) == {x: A. EX z. x = h(z)}"