src/HOL/TLA/ROOT.ML

revert to using eq_number_of_eq for simplification (Groebner_Examples.thy was broken)

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

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

use_thy "TLA";