author | wenzelm |
Tue, 24 Aug 1999 11:54:13 +0200 | |
changeset 7334 | a90fc1e5fb19 |
parent 7292 | dff3470c5c62 |
child 7583 | d1b40e0464b1 |
permissions | -rw-r--r-- |
(* Title: HOL/Real/ROOT 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 *) writeln"Root file for HOL/Real"; set proof_timing; time_use_thy "RealDef"; use "simproc.ML"; time_use_thy "Real"; time_use_thy "Hyperreal/Filter"; time_use_thy "Hyperreal/HyperDef";