src/ZF/Sum.thy
changeset 1401 0c439768f45c
parent 1108 22b256c8c9fb
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/Sum.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/Sum.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -9,10 +9,10 @@
     1.4  
     1.5  Sum = Bool + "simpdata" +
     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,Inr     :: i=>i
    1.13 +    case        :: [i=>i, i=>i, i]=>i
    1.14 +    Part        :: [i,i=>i] => i
    1.15  
    1.16  defs
    1.17      sum_def     "A+B == {0}*A Un {1}*B"