author | paulson |
Wed, 07 Jun 2000 12:14:18 +0200 | |
changeset 9043 | ca761fe227d8 |
parent 9013 | 9dd0274f76af |
child 9108 | 9fff97d29837 |
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 Linear real arithmetic is installed in RealBin.ML. *) time_use_thy "Real"; time_use_thy "Hyperreal/HyperDef";