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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
