Major Section: RELEASE-NOTES
The identity function case-split has been added. It is similar
to force but causes an immediate split of the top-level goal on
whether the indicated hypothesis is true.
Less important notes:
Minor bugs in the documentation were fixed.