--- a/src/HOL/Real/HahnBanach/ROOT.ML Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/ROOT.ML Fri Oct 08 16:40:27 1999 +0200
@@ -5,4 +5,5 @@
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
*)
+time_use_thy "Bounds";
time_use_thy "HahnBanach";