1signature spec_databaseLib =
2sig
3   datatype ''opt entry = Pending of Thm.thm * Term.term
4                        | Built of (''opt list * Thm.thm) list
5   val mk_spec_database:
6      (unit -> ''a) -> ''a -> (''a -> ''b) -> (''a -> ''a -> int) ->
7      (''a -> ''a -> Drule.rule) -> (Thm.thm -> Term.term) ->
8      (Thm.thm * Term.term -> Thm.thm) ->
9      (unit -> unit) * (''a -> unit) * (unit -> ''a) *
10      (Thm.thm * Term.term -> unit) *
11      (Term.term -> (bool * Thm.thm list) option) *
12      (unit -> (Term.term * ''a entry) list)
13end
14