--- a/src/HOL/Real/ROOT.ML Fri Feb 05 21:12:18 1999 +0100 +++ b/src/HOL/Real/ROOT.ML Fri Feb 05 21:12:45 1999 +0100 @@ -16,4 +16,5 @@ time_use_thy "RealAbs"; time_use_thy "RComplete"; -use_dir "Hyperreal"; +add_path "Hyperreal"; +use_thy "Filter";