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