isabelle: src/HOL/Integ/ROOT.ML@39e146ac224c (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";