?depth:int ->
?width:int ->
ProofEngineTypes.proof * ProofEngineTypes.goal ->
- (UriManager.uri option * Cic.conjecture list * Cic.term * Cic.term) *
- ProofEngineTypes.goal list
+ ProofEngineTypes.proof * ProofEngineTypes.goal list
val weight_age_ratio : int ref
val weight_age_counter: int ref
dbd:HMysql.dbd ->
pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
+val superposition_tac:
+ what:string -> other:string -> subterms_only:bool ->
+ demodulate:bool ->
+ ProofEngineTypes.proof * ProofEngineTypes.goal ->
+ ProofEngineTypes.proof * ProofEngineTypes.goal list
+
val get_stats: unit -> string