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
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