let change = ReductionTactics.change_tac
let clear = ProofEngineStructuralRules.clear
let clearbody = ProofEngineStructuralRules.clearbody
-let compare = DiscriminationTactics.compare_tac
let constructor = IntroductionTactics.constructor_tac
let contradiction = NegationTactics.contradiction_tac
let cut = PrimitiveTactics.cut_tac
-let decide_equality = DiscriminationTactics.decide_equality_tac
let decompose = EliminationTactics.decompose_tac
let demodulate = Saturation.demodulate_tac
let discriminate = DiscriminationTactics.discriminate_tac