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

On Fri, 28 Oct 2011, Johannes Hölzl wrote:

Am Donnerstag, den 27.10.2011, 10:49 -0500 schrieb James Frank:

I mentioned this to Makarius when I was building some HOL sessions with
usedir to get the PDFs, after which he pointed out that all the HOL
sessions are built and linked to at the bottom of There's no real
problem here.

However, I'll make a request here, and give some details below.

It would be nice if "~~/src/HOL/Probability/Borel_Space.thy" had the import
instead of simply "Multivariate_Analysis".

Okay, I changed this. Now it should be possible to build
Multivariate_Analysis and Probability with one ROOT.ML

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.


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