diff options
| author | Hugo Herbelin | 2015-09-09 11:21:55 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-11-10 16:39:01 +0100 |
| commit | 575fdab5df7c861692b19c62c2004c339c8621df (patch) | |
| tree | c95b7b789fa20ca464b69ceccddd6047ba1e4505 | |
| parent | bd1c976531ad6154339fff7e48e85dbe7951de23 (diff) | |
Listing separately changes from 8.5betas to final 8.5 and further
changes from final 8.5 to next version.
| -rw-r--r-- | CHANGES | 9 |
1 files changed, 9 insertions, 0 deletions
@@ -1,7 +1,16 @@ Changes beyond V8.5 =================== +Tactics + - Flag "Bracketing Last Introduction Pattern" is now on by default. +- New flag "Shrink Abstract" that minimalizes proofs generated by the abstract + tactical w.r.t. variables appearing in the body of the proof. + +Program + +- The "Shrink Obligations" flag now applies to all obligations, not only those + solved by the automatic tactic. Changes from V8.5beta2 to V8.5beta3 =================================== |