(* 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 by Jacques Fleuriot *) time_use_thy "Real";