1signature DB = 2sig 3 4 type term = Term.term 5 type thm = Thm.thm 6 datatype theory = datatype DB_dtype.theory 7 datatype class = datatype DB_dtype.class 8 type data = DB_dtype.data 9 10 11 val thy : string -> data list 12 val fetch : string -> string -> thm 13 val thms : string -> (string * thm) list 14 15 val theorem : string -> thm 16 val definition : string -> thm 17 val axiom : string -> thm 18 19 val axioms : string -> (string * thm) list 20 val theorems : string -> (string * thm) list 21 val definitions : string -> (string * thm) list 22 val find : string -> data list 23 val find_in : string -> data list -> data list 24 val matchp : (thm -> bool) -> string list -> data list 25 val matcher : (term -> term -> 'a) -> string list -> term -> data list 26 val match : string list -> term -> data list 27 val matches : term -> thm -> bool 28 val apropos : term -> data list 29 val apropos_in : term -> data list -> data list 30 val listDB : unit -> data list 31 32 33 val dest_theory : string -> theory 34 val bindl : string -> (string * thm * class) list -> unit 35 36 val CT : unit -> (string, (string, data list) Redblackmap.dict * 37 (string, data list) Redblackmap.dict) Redblackmap.dict 38 39 40end 41