| author | wenzelm |
| Fri, 25 Apr 1997 17:50:55 +0200 | |
| changeset 3061 | 25b2a895f864 |
| parent 2281 | e00c13a29eda |
| permissions | -rw-r--r-- |
(* Title: HOL/Integ/IntRingDefs.thy ID: $Id$ Author: Tobias Nipkow and Markus Wenzel Copyright 1996 TU Muenchen Provides the basic defs and thms for showing that int is a commutative ring. Most of it has been defined and shown already. *) IntRingDefs = Integ + Ring + instance int :: zero defs zero_int_def "zero::int == $# 0" end