--- a/src/HOL/Real/RealArith.thy Thu Dec 21 18:53:32 2000 +0100 +++ b/src/HOL/Real/RealArith.thy Thu Dec 21 18:57:12 2000 +0100 @@ -1,4 +1,4 @@ -theory RealArith = RealBin +theory RealArith = RealArith0 files "real_arith.ML": setup real_arith_setup