* Improved type-inference for theorem statement 'obtains': separate
parameter scope for of each clause.
This refers to 051b200f7578.
Here is an example based on the thread "Shadowing constants in obtains
clause" by Andreas Lochbihler 10-Dec-2014
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-December/msg00053.html
consts P :: "'a ⇒ bool"
consts Q :: "'a ⇒ bool"
lemma
assumes "(∃map::'a. P map) ∨ (∃map::'b. Q map)"
obtains map :: 'a where "P map" | map :: 'b where "Q map"
using assms by blast
This small improvement is a consequence of bigger changes elsewhere, for
more systematic treatment of 'obtain' clauses.
Further NEWS announcements will follow later ...
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
