[isabelle-dev] NEWS: improved 'obtain' with 'is' patterns

[Makarius]

* Command 'obtain' binds term abbreviations (via 'is' patterns) in the
proof body as well, abstracted over relevant parameters.


This refers e.g. to Isabelle/051b200f7578.

The multi-branch versions 'consider' and theorem 'obtains' do *not* 
support is-patterns -- as documented in the syntax diagrams.  The 
conceptual reason against it is the potential confusion that term bindings 
of all different branches end up in one proof body.  I do not mind to have 
that in principle, but the implementation in the presence of forked 
contexts is a bit difficult, and this is just a marginal feature anyway.


 	Makarius