src/HOL/TLA/ROOT.ML

uniform use of simultabeous use_thys;

(*  Title:      HOL/TLA/ROOT.ML

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

use_thys ["TLA"];