PR #1015 feat(tactic/basic): adds `contrapose` tactic

feat(tactic/basic): adds `contrapose` tactic

PatrickMassot committed 6 years ago

fix(tactic/push_neg): fix is_prop testing

PatrickMassot committed 6 years ago

Setup error message testing following Rob, add tests for `contrapose`

Patrick Massot committed 6 years ago

Merge remote-tracking branch 'community/master' into contrapose

Patrick Massot committed 6 years ago

refactor(tactic/interactive): move noninteractive success_if_fail_with_msg to tactic/core

robertylewis committed 6 years ago

Merge branch 'master' into contrapose

sgouezel committed 6 years ago

mathlib3 feat(tactic/basic): adds `contrapose` tactic #1015 Merged