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



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

- Johannes






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