[isabelle-dev] HOL-Proofs

[Makarius]

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