Mathlib v3 is deprecated. Go to Mathlib v4

Theorem imp_of_not_imp_not

Modification history

2020-04-08 17:46
src/tactic/push_neg.lean
feat(tactic/linter): add decidable_classical linter (#2352) …
Modified imp_of_not_imp_notView on Github →
2019-05-20 11:52
src/tactic/push_neg.lean
feat(tactic/basic): adds `contrapose` tactic (#1015) …
Added imp_of_not_imp_notView on Github →