isabelle: src/HOL/ex/IntRingDefs.thy@01386eb4eab0 (annotated)

5601 b6456ccd9e3e revised for new treatment of integers paulson parents: 5491 diff changeset	1	(* Title: HOL/ex/IntRingDefs.thy
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	2	ID: $Id$
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	3	Author: Tobias Nipkow and Markus Wenzel
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	4	Copyright 1996 TU Muenchen
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	5
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	6	Provides the basic defs and thms for showing that int is a commutative ring.
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	7	Most of it has been defined and shown already.
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	8	*)
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	9
5491 22f8331cdf47 revised treatment of integers paulson parents: 5078 diff changeset	10	IntRingDefs = Main + Ring +
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	11
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	12	instance int :: zero
5601 b6456ccd9e3e revised for new treatment of integers paulson parents: 5491 diff changeset	13	defs zero_int_def "zero::int == int 0"
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	14
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	15	end

author	wenzelm
	Tue, 05 Oct 1999 18:26:34 +0200
changeset 7742	01386eb4eab0
parent 5601	b6456ccd9e3e
permissions	-rw-r--r--