*To*: Johannes Hölzl <hoelzl at in.tum.de>*Subject*: Re: [isabelle] "usedir -b" on Probability: I have to add a relative path in Borel_Space.thy*From*: Makarius <makarius at sketis.net>*Date*: Fri, 28 Oct 2011 14:51:25 +0200 (CEST)*Cc*: James Frank <james.isa at gmx.com>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1319803866.2358.6.camel@vogelfrei>*References*: <4EA97D8C.3040000@gmx.com> <1319803866.2358.6.camel@vogelfrei>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

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

Makarius

**References**:

- Previous by Date: Re: [isabelle] "usedir -b" on Probability: I have to add a relative path in Borel_Space.thy
- Next by Date: [isabelle] local datatypes?
- Previous by Thread: Re: [isabelle] "usedir -b" on Probability: I have to add a relative path in Borel_Space.thy
- Next by Thread: Re: [isabelle] "usedir -b" on Probability: I have to add a relative path in Borel_Space.thy
- Cl-isabelle-users October 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list