src/ZF/ex/Integ.thy
changeset 753 ec86863e87c8
parent 532 851df239ac8b
child 1110 756aa2e81f6e
     1.1 --- a/src/ZF/ex/Integ.thy	Mon Nov 28 19:48:30 1994 +0100
     1.2 +++ b/src/ZF/ex/Integ.thy	Tue Nov 29 00:31:31 1994 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4      "$-"        ::      "[i,i]=>i"      (infixl 65)
     1.5      "$<"	:: 	"[i,i]=>o"  	(infixl 50)
     1.6  
     1.7 -rules
     1.8 +defs
     1.9  
    1.10      intrel_def
    1.11       "intrel == {p:(nat*nat)*(nat*nat). 		\