Search tactics for reasoning in Real Analysis



The following tactics are defined:
  • Contin will solve (Continuous_I H F)
  • Deriv will solve (Derivative_I H F F').


All these tactics are defined using eauto.