src/HOL/ex/IntRing.thy
author wenzelm
Fri, 05 Oct 2001 21:52:39 +0200
changeset 11701 3d51fbf81c17
parent 8936 a1c426541757
child 11868 56db9f3a6b3e
permissions -rw-r--r--
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;

(*  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 (Zero_int_def,zadd_int0,zadd_int0_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