HOL-Theorem-Prover/HOL

Ignore assumption directive for simplifier

Closed this issue · 0 comments

Something like

   simp[IgnAsm ‘pat’, th1]

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

Also

    simp[NoAsms,...]

should ignore all assumptions.