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

5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	1	(* Title: HOL/Integ/IntRingDefs.thy
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
5491 22f8331cdf47 revised treatment of integers paulson parents: 5078 diff changeset	13	defs zero_int_def "zero::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	oheimb
	Mon, 21 Sep 1998 23:25:27 +0200
changeset 5526	e7617b57a3e6
parent 5491	22f8331cdf47
child 5601	b6456ccd9e3e
permissions	-rw-r--r--