mathlib3
1bbed968 - doc(tactic/interactive): mention triv uses contradiction (#11502)

Commit

3 years ago

doc(tactic/interactive): mention triv uses contradiction (#11502) Adding the fact that `triv` tries `contradiction` to the docstring for `triv`.

Author

kbuzzard

Parents