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:
> 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
> instead of simply "Multivariate_Analysis".
Okay, I changed this. Now it should be possible to build
Multivariate_Analysis and Probability with one ROOT.ML
This archive was generated by a fusion of
Pipermail (Mailman edition) and