changeset 10752 | c4f1bf2acf4c |
parent 7978 | 1b99ee57d131 |
child 17260 | df7c3b1f390a |
--- a/src/HOL/Real/HahnBanach/ROOT.ML Sat Dec 30 22:03:47 2000 +0100 +++ b/src/HOL/Real/HahnBanach/ROOT.ML Sat Dec 30 22:13:18 2000 +0100 @@ -5,4 +5,4 @@ The Hahn-Banach theorem for real vector spaces (Isabelle/Isar). *) -time_use_thy "HahnBanach"; +with_path "../../Hyperreal" time_use_thy "HahnBanach";