src/ZF/Sum.thy
changeset 13220 62c899c77151
parent 5325 f7a5e06adea1
child 13240 bb5f4faea1f3
     1.1 --- a/src/ZF/Sum.thy	Tue Jun 18 17:58:21 2002 +0200
     1.2 +++ b/src/ZF/Sum.thy	Tue Jun 18 18:45:07 2002 +0200
     1.3 @@ -12,10 +12,11 @@
     1.4  global
     1.5  
     1.6  consts
     1.7 -    "+"         :: [i,i]=>i                     (infixr 65)
     1.8 -    Inl,Inr     :: i=>i
     1.9 -    case        :: [i=>i, i=>i, i]=>i
    1.10 -    Part        :: [i,i=>i] => i
    1.11 +    "+"     :: "[i,i]=>i"                     (infixr 65)
    1.12 +    Inl     :: "i=>i"
    1.13 +    Inr     :: "i=>i"
    1.14 +    "case"  :: "[i=>i, i=>i, i]=>i"
    1.15 +    Part    :: "[i,i=>i] => i"
    1.16  
    1.17  local
    1.18