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

Makarius 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 mailing list