src/ZF/ex/Integ.thy
changeset 532 851df239ac8b
parent 29 4ec9b266ccd1
child 753 ec86863e87c8
     1.1 --- a/src/ZF/ex/Integ.thy	Tue Aug 16 18:53:29 1994 +0200
     1.2 +++ b/src/ZF/ex/Integ.thy	Tue Aug 16 18:58:42 1994 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  The integers as equivalence classes over nat*nat.
     1.5  *)
     1.6  
     1.7 -Integ = Equiv + Arith +
     1.8 +Integ = EquivClass + Arith +
     1.9  consts
    1.10      intrel,integ::      "i"
    1.11      znat	::	"i=>i"		("$# _" [80] 80)