[isabelle-dev] HOL-Proofs slow

Makarius makarius at sketis.net
Mon Oct 22 13:12:56 CEST 2012

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 


Is there a way to bypass that in Main HOL?


More information about the isabelle-dev mailing list