case is defined using pattern-matching
authorlcp
Thu May 04 02:01:49 1995 +0200 (1995-05-04)
changeset 110822b256c8c9fb
parent 1107 f0ac02ffa21d
child 1109 380e9eb40db7
case is defined using pattern-matching
src/ZF/Sum.thy
     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)}"