src/HOL/Main.ML

New prover for transitive and reflexive-transitive closure of relations.
- Code in Provers/trancl.ML
- HOL: Simplifier set up to use it as solver

structure Main =
struct
  val thy = the_context ();
end;