author paulson
Thu, 08 Jul 1999 13:48:11 +0200
changeset 6921 78a2ce8fb8df
parent 5601 b6456ccd9e3e
child 8936 a1c426541757
permissions -rw-r--r--
Renaming of theorems from _nat0 to _int0 and _nat1 to _int1

(*  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_int0,zadd_int0_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)