[isabelle-dev] NEWS: improved type-inference for 'obtains'
makarius at sketis.net
Sun Jun 14 23:54:15 CEST 2015
* 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
consts P :: "'a ⇒ bool"
consts Q :: "'a ⇒ bool"
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 ...
More information about the isabelle-dev