Structure TheoryGraph

signature TheoryGraph =
sig

  type t
  type thy = {thyname : string}
  val toThy : string -> thy
  exception NotFound of thy

  val thy_compare : thy * thy -> order
  val ancestors : t -> thy -> thy HOLset.set
  (* val strict_dominators_map : t -> (thy, thy HOLset.set) *)
  val empty : t
  val insert : thy * thy list -> t -> t
  val member : t -> thy -> bool
  val parents : t -> thy -> thy HOLset.set

  val current : unit -> t

end

HOL 4, Kananaskis-13