let paramodulation_tactic = ref
(fun dbd ?full ?depth ?width status ->
raise (ProofEngineTypes.Fail (lazy "Not Ready yet...")));;
let term_is_equality = ref
(fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);;
let paramodulation_tactic = ref
(fun dbd ?full ?depth ?width status ->
raise (ProofEngineTypes.Fail (lazy "Not Ready yet...")));;
let term_is_equality = ref
(fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);;