--- a/src/HOL/TLA/ROOT.ML Sun Dec 30 23:07:31 2007 +0100
+++ b/src/HOL/TLA/ROOT.ML Mon Dec 31 19:36:29 2007 +0100
@@ -4,6 +4,5 @@
Adds the Temporal Logic of Actions to a database containing Isabelle/HOL.
*)
-val banner = "Temporal Logic of Actions";
+use_thy "TLA";
-time_use_thy "TLA";