[isabelle-dev] NEWS: improved 'obtain' with 'is' patterns
makarius at sketis.net
Mon Jun 15 00:21:59 CEST 2015
* 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.
More information about the isabelle-dev