On Sun, 21 Oct 2012, Makarius wrote:
Bijection then produced this:
The first bad revision is:
changeset: 49948:744934b818c7
user: haftmann
date: Sat Oct 20 09:12:16 2012 +0200
summary: moved quite generic material from theory Enum to more
appropriate places
I can't say for sure if this is a correct result of the bijection, but it
fits approximately in the time interval from my last successful (fast) test
of everything.
It is indeed the above changeset, notably the two code_simp invocations
here:
http://isabelle.in.tum.de/repos/isabelle/rev/744934b818c7#l9.7
Is there a way to bypass that in Main HOL?
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
