src/ZF/Sum.thy
changeset 35416 d8d7d1b785af
parent 32960 69916a850301
child 38514 bd9c4e8281ec
     1.1 --- a/src/ZF/Sum.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/ZF/Sum.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -11,21 +11,20 @@
     1.4  
     1.5  global
     1.6  
     1.7 -constdefs
     1.8 -  sum     :: "[i,i]=>i"                     (infixr "+" 65)
     1.9 +definition sum :: "[i,i]=>i" (infixr "+" 65) where
    1.10       "A+B == {0}*A Un {1}*B"
    1.11  
    1.12 -  Inl     :: "i=>i"
    1.13 +definition Inl :: "i=>i" where
    1.14       "Inl(a) == <0,a>"
    1.15  
    1.16 -  Inr     :: "i=>i"
    1.17 +definition Inr :: "i=>i" where
    1.18       "Inr(b) == <1,b>"
    1.19  
    1.20 -  "case"  :: "[i=>i, i=>i, i]=>i"
    1.21 +definition "case" :: "[i=>i, i=>i, i]=>i" where
    1.22       "case(c,d) == (%<y,z>. cond(y, d(z), c(z)))"
    1.23  
    1.24    (*operator for selecting out the various summands*)
    1.25 -  Part    :: "[i,i=>i] => i"
    1.26 +definition Part :: "[i,i=>i] => i" where
    1.27       "Part(A,h) == {x: A. EX z. x = h(z)}"
    1.28  
    1.29  local