Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-06 03:44 06f47783

View on Github →

feat(tactic/tauto): handle or in goal

Estimated changes

Modified tactic/interactive.lean

added theorem tactic.interactive.iff.trans

added theorem tactic.interactive.imp.swap

added theorem tactic.interactive.imp_not_comm

added theorem tactic.interactive.not_and_distrib'

added theorem tactic.interactive.not_and_distrib

added theorem tactic.interactive.not_and_of_not_or_not

added theorem tactic.interactive.not_or_distrib

added theorem tactic.interactive.or_iff_not_imp_left

added theorem tactic.interactive.or_iff_not_imp_right

Modified tests/examples.lean