isabelle: src/HOL/Real/ROOT.ML@351ba950d4d9 (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
10043 a0364652e115 Updated Files with new theorems fleuriot parents: 9430 diff changeset	6	Construction of the Reals using Dedekind Cuts, Ultrapower Construction
10094 22f201e9ec7a proper Hyperreal setup; wenzelm parents: 10043 diff changeset	7	of the hyperreals, and mechanization of Nonstandard Real Analysis
10043 a0364652e115 Updated Files with new theorems fleuriot parents: 9430 diff changeset	8	by Jacques Fleuriot
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	9	*)
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	10
10094 22f201e9ec7a proper Hyperreal setup; wenzelm parents: 10043 diff changeset	11	with_path "Hyperreal" time_use_thy "Hyperreal";