jellooo038
commented
11 months ago - Integrated restricted automated proof search for 'By ...' clause into existing tactics
- Improved tactics
- simplified notation 'Obtain' tactic
- 'Contradiction' tactic now attempts to find contradiction to previous statement
- Added 'Since ...' clause that accepts statements instead of references as in 'By ...' clause
- Proof of concept for having to explicitly invoke definitions in order to use them in [SupAndInf.v]