--- 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>"