src/ZF/Sum.thy
changeset 124 858ab9a9b047
parent 0 a5a9c433f639
child 753 ec86863e87c8
--- a/src/ZF/Sum.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Sum.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -7,7 +7,7 @@
 "Part" primitive for simultaneous recursive type definitions
 *)
 
-Sum = Bool +
+Sum = Bool + "simpdata" +
 consts
     "+"    	:: "[i,i]=>i"      		(infixr 65)
     Inl,Inr     :: "i=>i"