* 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
