(* Title: TLA/ROOT.ML Adds the Temporal Logic of Actions to a database containing Isabelle/HOL. *) val banner = "Temporal Logic of Actions"; time_use_thy "TLA";