# HG changeset patch
# User paulson
# Date 941022143 -7200
# Node ID 95e1de322e82efbd182838bba625608b066468ed
# Parent  3aca6352f063ae946600e039f06baa616954e069
TEMPORARY use of Addsimps

diff -r 3aca6352f063 -r 95e1de322e82 src/HOL/Real/ROOT.ML
--- 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];