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