(* Title: HOL/Real/ROOT.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of CambridgeConstruction of the Reals using Dedekind Cuts, by Jacques Fleuriot*)with_path "Hyperreal" use_thy "HyperDef";