src/ZF/Sum.thy
changeset 753 ec86863e87c8
parent 124 858ab9a9b047
child 1108 22b256c8c9fb
     1.1 --- a/src/ZF/Sum.thy	Mon Nov 28 19:48:30 1994 +0100
     1.2 +++ b/src/ZF/Sum.thy	Tue Nov 29 00:31:31 1994 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4      case        :: "[i=>i, i=>i, i]=>i"
     1.5      Part        :: "[i,i=>i] => i"
     1.6  
     1.7 -rules
     1.8 +defs
     1.9      sum_def     "A+B == {0}*A Un {1}*B"
    1.10      Inl_def     "Inl(a) == <0,a>"
    1.11      Inr_def     "Inr(b) == <1,b>"