--- a/src/HOL/Real/RealArith.thy Fri Dec 01 19:44:48 2000 +0100 +++ b/src/HOL/Real/RealArith.thy Fri Dec 01 19:53:29 2000 +0100 @@ -1,4 +1,3 @@ - theory RealArith = RealBin files "real_arith.ML":