author | wenzelm |
Mon, 20 Oct 1997 11:14:55 +0200 | |
changeset 3945 | ae9c61d69888 |
parent 3807 | 82a99b090d9d |
child 4477 | b3e5857d8d99 |
permissions | -rw-r--r-- |
(* 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; reset global_names; use_thy "TLA"; val TLA_build_completed = ();