val auto :
?depth:int ->
?width:int ->
- ?paramodulation:string -> dbd:HMysql.dbd -> unit -> ProofEngineTypes.tactic
+ ?paramodulation:string ->
+ ?full:string -> dbd:HMysql.dbd -> unit -> ProofEngineTypes.tactic
val change :
pattern:ProofEngineTypes.pattern ->
ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic