ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
authorlcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532851df239ac8b
parent 531 e24f47f8938e
child 533 7357160bc56a
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
src/ZF/ROOT.ML
src/ZF/ex/Integ.thy
     1.1 --- a/src/ZF/ROOT.ML	Tue Aug 16 18:53:29 1994 +0200
     1.2 +++ b/src/ZF/ROOT.ML	Tue Aug 16 18:58:42 1994 +0200
     1.3 @@ -42,6 +42,7 @@
     1.4  
     1.5  use_thy "InfDatatype";
     1.6  use_thy "List";
     1.7 +use_thy "EquivClass";
     1.8  
     1.9  (*printing functions are inherited from FOL*)
    1.10  print_depth 8;
     2.1 --- a/src/ZF/ex/Integ.thy	Tue Aug 16 18:53:29 1994 +0200
     2.2 +++ b/src/ZF/ex/Integ.thy	Tue Aug 16 18:58:42 1994 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  The integers as equivalence classes over nat*nat.
     2.5  *)
     2.6  
     2.7 -Integ = Equiv + Arith +
     2.8 +Integ = EquivClass + Arith +
     2.9  consts
    2.10      intrel,integ::      "i"
    2.11      znat	::	"i=>i"		("$# _" [80] 80)