[isabelle-dev] NEWS: improved type-inference for 'obtains'

[Makarius]

* 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