| author | paulson |
| Fri, 11 Sep 1998 16:25:40 +0200 | |
| changeset 5479 | 5a5dfb0f0d7d |
| parent 5078 | 7b5ea59c0275 |
| child 5491 | 22f8331cdf47 |
| permissions | -rw-r--r-- |
| 5078 | 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 |