src/HOL/ex/IntRing.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/IntRing.thy	Thu Jun 25 13:57:34 1998 +0200
@@ -0,0 +1,19 @@
+(*  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 = IntRingDefs + Lagrange +
+
+instance int :: add_semigroup (zadd_assoc)
+instance int :: add_monoid (zero_int_def,zadd_0,zadd_0_right)
+instance int :: add_group (left_inv_int,minus_inv_int)
+instance int :: add_agroup (zadd_commute)
+instance int :: ring (zmult_assoc,zadd_zmult_distrib2,zadd_zmult_distrib)
+instance int :: cring (zmult_commute)
+
+end