equal
deleted
inserted
replaced
|
1 (* Title: HOL/Integ/IntRing.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow and Markus Wenzel |
|
4 Copyright 1996 TU Muenchen |
|
5 |
|
6 The integers form a commutative ring. |
|
7 With an application of Lagrange's lemma. |
|
8 *) |
|
9 |
|
10 IntRing = IntRingDefs + Lagrange + |
|
11 |
|
12 instance int :: add_semigroup (zadd_assoc) |
|
13 instance int :: add_monoid (zero_int_def,zadd_0,zadd_0_right) |
|
14 instance int :: add_group (left_inv_int,minus_inv_int) |
|
15 instance int :: add_agroup (zadd_commute) |
|
16 instance int :: ring (zmult_assoc,zadd_zmult_distrib2,zadd_zmult_distrib) |
|
17 instance int :: cring (zmult_commute) |
|
18 |
|
19 end |