isabelle: src/HOL/Real/ROOT.ML@dff3470c5c62 (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
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	7	*)
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	8
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	9	writeln"Root file for HOL/Real";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	10
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	11	set proof_timing;
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: 5078 diff changeset	12	time_use_thy "RealDef";
6490 4961ecbaaff7 improved load paths; wenzelm parents: 6349 diff changeset	13	use "simproc.ML";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	14	time_use_thy "RComplete";
6490 4961ecbaaff7 improved load paths; wenzelm parents: 6349 diff changeset	15	time_use_thy "Hyperreal/Filter";
7219 4e3f386c2e37 inserted Id: lines paulson parents: 6490 diff changeset	16	time_use_thy "Hyperreal/HyperDef";

author	paulson
	Thu, 19 Aug 1999 18:36:41 +0200
changeset 7292	dff3470c5c62
parent 7219	4e3f386c2e37
child 7334	a90fc1e5fb19
permissions	-rw-r--r--