NEWS
changeset 60459 2761a2249c83
parent 60455 0c4077939278
child 60460 abee0de69a89
     1.1 --- a/NEWS	Sat Jun 13 20:07:54 2015 +0200
     1.2 +++ b/NEWS	Sat Jun 13 22:42:23 2015 +0200
     1.3 @@ -38,6 +38,11 @@
     1.4  * New command 'supply' supports fact definitions during goal refinement
     1.5  ('apply' scripts).
     1.6  
     1.7 +* New command 'consider' states rules for generalized elimination and
     1.8 +case splitting. This is like a toplevel statement "theorem obtains" used
     1.9 +within a proof body; or like a multi-branch 'obtain' without activation
    1.10 +of the local context elements yet.
    1.11 +
    1.12  * Proof method "cases" allows to specify the rule as first entry of
    1.13  chained facts.  This is particularly useful with 'consider':
    1.14