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