HOL-Proofs has become very slow, see
http://www4.in.tum.de/~wenzelm/test/stats/mac-poly64-M8/HOL-Proofs.png


I first thought it would be related to 1167c1157a5b (haftmann on src/Pure/Proof/extraction.ML), which is not immediately easy to follow in every detail.


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.


        Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to