[isabelle-dev] Towards the next release
gerwin.klein at nicta.com.au
Thu May 3 00:42:35 CEST 2012
On 02/05/2012, at 11:11 PM, Makarius wrote:
> On Tue, 17 Apr 2012, Gerwin Klein wrote:
>> There is a third small thing that I will discuss separately with Florian: there is a bug in the code generator setup in Isabelle2011-1 somewhere in generating narrowing lemmas. It is triggered for records with more than ~530 fields where it constructs a lemma of the form "f ty = g a b .. aa ab .. tw tx ty tz .." where the ty on the rhs is different to the ty on the left. It should be easy to fix once I manage to trace down where it is actually constructed and I haven't checked yet if it still occurs in the development version.
> Is this still an open issue for the release?
It can wait for after the release. I don't think anyone is blocked on it.
More information about the isabelle-dev