Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Integ/IntRing.thy
author oheimb
Sat, 15 Feb 1997 16:04:33 +0100
changeset 2626 373daa468a74
parent 2281 e00c13a29eda
permissions -rw-r--r--
added del_congs

(*  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
isabelle