| author | wenzelm |
| Tue, 05 Oct 1999 18:26:34 +0200 | |
| changeset 7742 | 01386eb4eab0 |
| parent 6921 | 78a2ce8fb8df |
| child 8936 | a1c426541757 |
| permissions | -rw-r--r-- |
| 5078 | 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) |
|
|
6921
78a2ce8fb8df
Renaming of theorems from _nat0 to _int0 and _nat1 to _int1
paulson
parents:
5601
diff
changeset
|
13 |
instance int :: add_monoid (zero_int_def,zadd_int0,zadd_int0_right) |
| 5078 | 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 |