--- a/src/HOL/Real/RealDef.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/Real/RealDef.thy Fri Jun 17 16:12:49 2005 +0200 @@ -9,7 +9,7 @@ theory RealDef imports PReal -files ("real_arith.ML") +uses ("real_arith.ML") begin constdefs