author | paulson |
Wed, 27 Oct 1999 13:02:23 +0200 | |
changeset 7946 | 95e1de322e82 |
parent 7945 | 3aca6352f063 |
child 7947 | b999c1ab9327 |
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];