[isabelle-dev] Towards the next release
makarius at sketis.net
Wed May 2 15:11:17 CEST 2012
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?
More information about the isabelle-dev