author | paulson |
Thu, 08 Jul 1999 13:48:11 +0200 | |
changeset 6921 | 78a2ce8fb8df |
parent 5601 | b6456ccd9e3e |
permissions | -rw-r--r-- |
5601 | 1 |
(* Title: HOL/ex/IntRingDefs.thy |
5078 | 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 |
||
5491 | 10 |
IntRingDefs = Main + Ring + |
5078 | 11 |
|
12 |
instance int :: zero |
|
5601 | 13 |
defs zero_int_def "zero::int == int 0" |
5078 | 14 |
|
15 |
end |