1.1 --- a/src/HOL/Real/ROOT.ML	Wed Oct 27 12:50:48 1999 +0200
     1.2 +++ b/src/HOL/Real/ROOT.ML	Wed Oct 27 13:02:23 1999 +0200
     1.3 @@ -15,3 +15,7 @@
     1.4  time_use_thy "Real";
     1.5  time_use_thy "Hyperreal/Filter";
     1.6  time_use_thy "Hyperreal/HyperDef";
     1.7 +
     1.8 +(*FIXME: move to RealBin and eliminate all references to 0r, 1r in 
     1.9 +  descendant theories*)
    1.10 +Addsimps [zero_eq_numeral_0, one_eq_numeral_1];