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:
Hi,

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
http://isabelle.in.tum.de/dist/library/HOL/index.html. 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
     "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis",
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.


	Makarius


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