Ignore assumption directive for simplifier

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.

https://hol-theorem-prover.org

Other

621 stars 140 forks source link

Ignore assumption directive for simplifier #1220

Closed mn200 closed 3 days ago

mn200 commented 5 months ago

Something like

   simp[IgnAsm ‘pat’, th1]

should apply the simplifier, while ignoring the assumption(s) matching pat.

Also

    simp[NoAsms,...]

should ignore all assumptions.