author | nipkow |
Thu, 12 Oct 2000 18:38:23 +0200 | |
changeset 10212 | 33fe2d701ddd |
parent 10094 | 22f201e9ec7a |
child 10752 | c4f1bf2acf4c |
permissions | -rw-r--r-- |
(* Title: HOL/Real/ROOT.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge Construction of the Reals using Dedekind Cuts, Ultrapower Construction of the hyperreals, and mechanization of Nonstandard Real Analysis by Jacques Fleuriot *) with_path "Hyperreal" time_use_thy "Hyperreal";