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

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