--- a/src/HOL/ex/IntRing.thy Fri Apr 16 19:04:17 2004 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(* Title: HOL/Integ/IntRing.thy
- ID: $Id$
- Author: Tobias Nipkow and Markus Wenzel
- Copyright 1996 TU Muenchen
-
-The integers form a commutative ring.
-With an application of Lagrange's lemma.
-*)
-
-IntRing = Ring + Lagrange +
-
-instance int :: add_semigroup (zadd_assoc)
-instance int :: add_monoid (zadd_0,zadd_0_right)
-instance int :: add_group {|Auto_tac|}
-instance int :: add_agroup (zadd_commute)
-instance int :: ring (zmult_assoc,zadd_zmult_distrib2,zadd_zmult_distrib)
-instance int :: cring (zmult_commute)
-
-end