author | paulson |
Fri, 27 Nov 1998 11:24:27 +0100 | |
changeset 5979 | 11cbf236ca16 |
parent 5588 | a3ab526bb891 |
child 6251 | 4d89d4f0ab17 |
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 *) HOL_build_completed; (*Make examples fail if HOL did*) writeln"Root file for HOL/Real"; set proof_timing; time_use_thy "RealDef"; use "simproc"; time_use_thy "RealAbs"; time_use_thy "RComplete"; use_dir "Hyperreal";