[isabelle-dev] Towards the next release

[Gerwin Klein]

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.

Gerwin