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