Mathlib v3 is deprecated. Go to Mathlib v4

Theorem tactic.interactive.imp_not_comm

Modification history

2018-07-06 03:44
tactic/interactive.lean
feat(tactic/cache): split cache related tactics off from `tactic.interactive`
Deleted tactic.interactive.imp_not_commView on Github →
2018-07-06 03:44
tactic/interactive.lean
feat(tactic/tauto): handle `or` in goal
Added tactic.interactive.imp_not_commView on Github →