# 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.
Makarius

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