--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Real/RealArith.thy Tue Jul 25 00:06:46 2000 +0200 @@ -0,0 +1,7 @@ + +theory RealArith = RealBin +files "real_arith.ML": + +setup real_arith_setup + +end