isabelle: src/HOL/Real/ROOT.ML@c169cd21fe42 (annotated)

5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	1	(* Title: HOL/Real/ROOT
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: Lawrence C Paulson, Cambridge University Computer Laboratory
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	4	Copyright 1998 University of Cambridge
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	5
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	6	Construction of the Reals using Dedekind Cuts, by Jacques Fleuriot
7583 d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete. nipkow parents: 7334 diff changeset	7
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete. nipkow parents: 7334 diff changeset	8	Linear real arithmetic is installed in RealBin.ML.
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	9	*)
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	10
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	11	writeln"Root file for HOL/Real";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	12
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: 5078 diff changeset	13	time_use_thy "RealDef";
6490 4961ecbaaff7 improved load paths; wenzelm parents: 6349 diff changeset	14	use "simproc.ML";
7334 a90fc1e5fb19 Real/Real.thy main entry point; wenzelm parents: 7292 diff changeset	15	time_use_thy "Real";
6490 4961ecbaaff7 improved load paths; wenzelm parents: 6349 diff changeset	16	time_use_thy "Hyperreal/Filter";
7219 4e3f386c2e37 inserted Id: lines paulson parents: 6490 diff changeset	17	time_use_thy "Hyperreal/HyperDef";
7946 95e1de322e82 TEMPORARY use of Addsimps paulson parents: 7933 diff changeset	18
95e1de322e82 TEMPORARY use of Addsimps paulson parents: 7933 diff changeset	19	(*FIXME: move to RealBin and eliminate all references to 0r, 1r in
95e1de322e82 TEMPORARY use of Addsimps paulson parents: 7933 diff changeset	20	descendant theories*)
95e1de322e82 TEMPORARY use of Addsimps paulson parents: 7933 diff changeset	21	Addsimps [zero_eq_numeral_0, one_eq_numeral_1];

author	paulson
	Sat, 04 Mar 2000 12:02:41 +0100
changeset 8340	c169cd21fe42
parent 7946	95e1de322e82
child 8856	435187ffc64e
permissions	-rw-r--r--