| changeset 5078 | 7b5ea59c0275 |
| child 5491 | 22f8331cdf47 |
| 5077:71043526295f | 5078:7b5ea59c0275 |
|---|---|
1 (* Title: HOL/Integ/IntRingDefs.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow and Markus Wenzel |
|
4 Copyright 1996 TU Muenchen |
|
5 |
|
6 Provides the basic defs and thms for showing that int is a commutative ring. |
|
7 Most of it has been defined and shown already. |
|
8 *) |
|
9 |
|
10 IntRingDefs = Integ + Ring + |
|
11 |
|
12 instance int :: zero |
|
13 defs zero_int_def "zero::int == $# 0" |
|
14 |
|
15 end |