1
(* Title: TLA/ROOT.ML
2
3
Adds the Temporal Logic of Actions to a database containing Isabelle/HOL.
4
*)
5
6
val banner = "Temporal Logic of Actions";
7
8
time_use_thy "TLA";