On Wed, 14 May 2014, Tobias Nipkow wrote:
This is what I did interactively: starting from Pure I loaded Proofs.thy
first and then Main.thy. Maybe this did not really switch proof terms
on?
That should do the right thing. The remaining explanation is that PIDE is
less aggressive in proof parallelization and less heap was used. That
performance profile is specific to for HOL-Proofs: more parallelism
requires more space, and some years ago HOL-Proofs actually had
parallel_proofs = 0.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
