Skip to content
  • Robbert Krebbers's avatar
    Remove elem_of_tactic that uses intuition. · 8ee34859
    Robbert Krebbers authored
    This one (previously solve_elem_of) was hardly used. The tactic that uses
    naive_solver (previously esolve_elem_of, now solve_elem_of) has been
    extended with flags to say which hypotheses should be cleared/kept.
    8ee34859