src/HOL/TLA/ROOT.ML

ex/Antiquote.thy made new-style theory;
removed ex/Antiquote.ML;

(*  Title:      TLA/ROOT.ML

Adds the Temporal Logic of Actions to a database containing Isabelle/HOL.
*)

val banner = "Temporal Logic of Actions";

use_thy "TLA";