src/HOL/Integ/IntRing.thy
author wenzelm
Thu Jan 23 14:19:16 1997 +0100 (1997-01-23)
changeset 2545 d10abc8c11fb
parent 2281 e00c13a29eda
permissions -rw-r--r--
added AxClasses test;
nipkow@2281
     1
(*  Title:      HOL/Integ/IntRing.thy
nipkow@2281
     2
    ID:         $Id$
nipkow@2281
     3
    Author:     Tobias Nipkow and Markus Wenzel
nipkow@2281
     4
    Copyright   1996 TU Muenchen
nipkow@2281
     5
nipkow@2281
     6
The integers form a commutative ring.
nipkow@2281
     7
With an application of Lagrange's lemma.
nipkow@2281
     8
*)
nipkow@2281
     9
nipkow@2281
    10
IntRing = IntRingDefs + Lagrange +
nipkow@2281
    11
nipkow@2281
    12
instance int :: add_semigroup (zadd_assoc)
nipkow@2281
    13
instance int :: add_monoid (zero_int_def,zadd_0,zadd_0_right)
nipkow@2281
    14
instance int :: add_group (left_inv_int,minus_inv_int)
nipkow@2281
    15
instance int :: add_agroup (zadd_commute)
nipkow@2281
    16
instance int :: ring (zmult_assoc,zadd_zmult_distrib2,zadd_zmult_distrib)
nipkow@2281
    17
instance int :: cring (zmult_commute)
nipkow@2281
    18
nipkow@2281
    19
end