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