isabelle: src/HOL/Integ/ROOT.ML@97601cf26262 (annotated)

1465 5d7a7e439cec expanded tabs clasohm parents: 1351 diff changeset	1	(* Title: HOL/Integ/ROOT
925 15539deb6863 new version of HOL/Integ with curried function application clasohm parents: diff changeset	2	ID: $Id$
1465 5d7a7e439cec expanded tabs clasohm parents: 1351 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
925 15539deb6863 new version of HOL/Integ with curried function application clasohm parents: diff changeset	4	Copyright 1995 University of Cambridge
15539deb6863 new version of HOL/Integ with curried function application clasohm parents: diff changeset	5
1165 97b2bb5d43c3 renamed CHOL to HOL clasohm parents: 1025 diff changeset	6	The Integers in HOL (ported from ZF by Riccardo Mattolini)
925 15539deb6863 new version of HOL/Integ with curried function application clasohm parents: diff changeset	7	*)
15539deb6863 new version of HOL/Integ with curried function application clasohm parents: diff changeset	8
1165 97b2bb5d43c3 renamed CHOL to HOL clasohm parents: 1025 diff changeset	9	HOL_build_completed; (Cause examples to fail if HOL did)
925 15539deb6863 new version of HOL/Integ with curried function application clasohm parents: diff changeset	10
1632 39e146ac224c Binary integers and their numeric syntax paulson parents: 1465 diff changeset	11	time_use_thy "Bin";
2280 eb2ba30c2981 Moved the Rings stuff from ex to Integ and showed that int::cring. nipkow parents: 1632 diff changeset	12	time_use_thy "IntRing";

author	paulson
	Thu, 20 Nov 1997 11:03:26 +0100
changeset 4242	97601cf26262
parent 2280	eb2ba30c2981
child 5078	7b5ea59c0275
permissions	-rw-r--r--