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

9108 9fff97d29837 bind_thm(s); wenzelm parents: 9043 diff changeset	1	(* Title: HOL/Real/ROOT.ML
5078 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
9108 9fff97d29837 bind_thm(s); wenzelm parents: 9043 diff changeset	11	with_path "Hyperreal" use_thy "HyperDef";