author | wenzelm |
Mon, 16 Nov 1998 10:41:08 +0100 | |
changeset 5869 | b279a84ac11c |
parent 5601 | b6456ccd9e3e |
permissions | -rw-r--r-- |
(* Title: HOL/ex/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 = Main + Ring + instance int :: zero defs zero_int_def "zero::int == int 0" end