[isabelle-dev] Towards the next release

[Makarius]

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?


 	Makarius