1signature TheoryGraph =
2sig
3
4  type t
5  type thy = {thyname : string}
6  val toThy : string -> thy
7  exception NotFound of thy
8
9  val thy_compare : thy * thy -> order
10  val ancestors : t -> thy -> thy HOLset.set
11  (* val strict_dominators_map : t -> (thy, thy HOLset.set) *)
12  val empty : t
13  val insert : thy * thy list -> t -> t
14  val member : t -> thy -> bool
15  val parents : t -> thy -> thy HOLset.set
16
17  val current : unit -> t
18
19end
20