src/HOL/Real/ROOT.ML
author wenzelm
Tue May 30 16:08:38 2000 +0200 (2000-05-30)
changeset 9000 c20d58286a51
parent 8856 435187ffc64e
child 9013 9dd0274f76af
permissions -rw-r--r--
cleaned up;
paulson@5078
     1
(*  Title:      HOL/Real/ROOT
paulson@5078
     2
    ID:         $Id$
paulson@5078
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5078
     4
    Copyright   1998  University of Cambridge
paulson@5078
     5
paulson@5078
     6
Construction of the Reals using Dedekind Cuts, by Jacques Fleuriot
nipkow@7583
     7
nipkow@7583
     8
Linear real arithmetic is installed in RealBin.ML.
paulson@5078
     9
*)
paulson@5078
    10
paulson@5588
    11
time_use_thy "RealDef";
wenzelm@6490
    12
use          "simproc.ML";
wenzelm@7334
    13
time_use_thy "Real";
paulson@7219
    14
time_use_thy "Hyperreal/HyperDef";
paulson@7946
    15
paulson@7946
    16
(*FIXME: move to RealBin and eliminate all references to 0r, 1r in 
paulson@7946
    17
  descendant theories*)
paulson@7946
    18
Addsimps [zero_eq_numeral_0, one_eq_numeral_1];