diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 5 |
1 files changed, 5 insertions, 0 deletions
@@ -56,12 +56,17 @@ Tactics independently of the number of ipats, which has itself to be less than the number of new hypotheses (possible source of incompatibilities; former behavior obtainable by "Unset Injection L2R Pattern Order"). +- New tactic "rewrite_strat" for generalized rewriting with user-defined + strategies, subsumming autorewrite. Program - "Solve Obligations using" changed to "Solve Obligations with", consistent with "Proof with". - Program Lemma, Definition now respect automatic introduction. +- Add/document "Set Hide Obligations" (to hide obligations in the final + term inside an implicit argument) and "Set Shrink Obligations" (to + minimize dependencies of obligations defined by tactics). Notations |