Re: [isabelle] "usedir -b" on Probability: I have to add a relative path in Borel_Space.thy
Okay, I changed this. Now it should be possible to build
Multivariate_Analysis and Probability with one ROOT.ML
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.
Thanks for the tips.
Just to perform the canonical running gag: "now" means version
fc3c7db5bb2f in the Isabelle repository, and to benefit from it you
need to wait for the next official release, or switch to alpha/beta
testing of development snapshots. The latter are discussed on
isabelle-dev, not isabelle-users.
That's why I ask now, to try to get it in the next release.
I looked at the repository a few weeks back, and again now. I can't figure it out, and there's not much motivation; I don't want to try and build any sources for Cygwin, plus everything is working good anyway.
I'm on the dev mailing list. I saw the recent exchange on the "non-terminating function".
The law of the excluded middle, you gotta have it, and Isabelle has it, so I keep hanging around. If you can't know something's true, at least you can know sometimes that it's not true. Who wants to spend their life trying to prove something true when it's not true? And, I suppose, false, when it's not false. It's nice to know when it's useless to try and work out the details, because there are no details that can ever be worked out.
This archive was generated by a fusion of
Pipermail (Mailman edition) and