1(* ========================================================================= *)
2(* A STORE IN WHICH TO CACHE UNIT THEOREMS                                   *)
3(* Copyright (c) 2001-2004 Joe Hurd.                                         *)
4(* ========================================================================= *)
5
6signature mlibUnits =
7sig
8
9type 'a pp   = 'a mlibUseful.pp
10type formula = mlibTerm.formula
11type thm     = mlibThm.thm
12
13type units
14
15val empty      : units
16val add        : thm -> units -> units
17val addl       : thm list -> units -> units
18val subsumes   : units -> formula -> thm option
19val contr      : units -> thm -> thm option
20val prove      : units -> formula list -> thm list option
21val demod      : units -> thm -> thm
22val info       : units -> string
23val pp_units   : units pp
24
25end
26