isabelle: src/HOL/Real/ROOT.ML@d3671b878828 (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
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10094 diff changeset	6	Construction of the Reals using Dedekind Cuts
c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10094 diff changeset	7	by Jacques Fleuriot
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	8	*)
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	9
12733 611ab32b2176 Real/Complex_Numbers.thy; wenzelm parents: 10752 diff changeset	10	no_document time_use_thy "Ring_and_Field";
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10094 diff changeset	11	time_use_thy "Real";