isabelle: src/HOL/Integ/IntRingDefs.thy@44f01b718eab (annotated)

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