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