TEMPORARY use of Addsimps

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