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