src/HOL/TLA/ROOT.ML

replaced Term.equiv_types by Type.similar_types;

(*  Title:      HOL/TLA/ROOT.ML
    ID:         $Id$

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

val banner = "Temporal Logic of Actions";

time_use_thy "TLA";