--- a/src/HOL/Real/HahnBanach/ROOT.ML Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/ROOT.ML Fri Oct 29 20:18:34 1999 +0200
@@ -5,5 +5,4 @@
The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
*)
-time_use_thy "Bounds";
time_use_thy "HahnBanach";