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

- Johannes
Thanks.

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

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.

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

--James






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