# HG changeset patch
# User wenzelm
# Date 918245565 -3600
# Node ID 4d89d4f0ab17f7fefbbf88dbb48b3b211278ce48
# Parent  354848db4052ba975e06f21cd59a4c391dbceca2
add_path;

diff -r 354848db4052 -r 4d89d4f0ab17 src/HOL/Real/ROOT.ML
--- 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";