src/HOL/TLA/ROOT.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TLA/ROOT.ML	Wed Oct 08 11:50:33 1997 +0200
@@ -0,0 +1,17 @@
+(*  Title:      TLA/ROOT.ML
+
+Adds the Temporal Logic of Actions to a database containing Isabelle/HOL.
+*)
+
+val banner = "Temporal Logic of Actions";
+
+(*
+   raise the ambiguity level to avoid ambiguity warnings;
+   since Trueprop and TrueInt have both empty syntax, there is
+   an unavoidable ambiguity in the TLA (actually, Intensional) grammar.
+*)
+Syntax.ambiguity_level := 10000;
+
+use_thy "TLA";
+
+val TLA_build_completed = ();