Re: [isabelle] "usedir -b" on Probability: I have to add a relative path in Borel_Space.thy

On Thu, 27 Oct 2011, James Frank wrote:

I thought about buying an i7 notebook, and then I built the heap for Multivariate_Analysis and used it as my logic, which solved my need for practical speed.

Pre-built heaps generally improve the memory situation, because all results are maximally shared in the end. So a heap of several GB will end up as a few hundred MB that can then be used in interactive sessions.

I made a ROOT.ML composed of the ROOT.MLs from Library, Old_Number_Theory, Algebra, Lattice, Matrix, Multivariate_Analysis, NSA, Number_Theory, Probability, and ZF.

Two fine points here:

  * A single simulatenous use_thys provides more opportinity for
    parallelism in batch mode.

  * Some sessions share certain popular theory names, and loading them
    together will lead to surprises, due to the flat theory name space.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.