src/HOL/Algebra/IntRing.thy
changeset 25919 8b1c0d434824
parent 24131 1099f6c73649
child 27713 95b36bfe7fc4
--- a/src/HOL/Algebra/IntRing.thy	Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Tue Jan 15 16:19:23 2008 +0100
@@ -5,7 +5,7 @@
 *)
 
 theory IntRing
-imports QuotRing IntDef
+imports QuotRing Int
 begin