*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] "usedir -b" on Probability: I have to add a relative path in Borel_Space.thy*From*: James Frank <james.isa at gmx.com>*Date*: Thu, 27 Oct 2011 10:49:32 -0500*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:6.0.2) Gecko/20110902 Thunderbird/6.0.2

Hi,

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

Anyway, here's what led to this request.

One thing leads to another.

My ROOT.ML gets one error in the build using the command, isabelle usedir -b HOL HOL_LibOntAlgLatMatMvNsaNtPrbZf. To get it to build, I have to edit Borel_Space.thy as explained above. Below, I've included the contents of my ROOT.ML. Thanks, James (* From ~~/src/HOL/Library/ROOT.ML *) use_thys [ "~~/src/HOL/Library/Library", "~~/src/HOL/Library/List_Cset", "~~/src/HOL/Library/List_Prefix", "~~/src/HOL/Library/List_lexord", "~~/src/HOL/Library/Sublist_Order", "~~/src/HOL/Library/Product_Lattice", "~~/src/HOL/Library/Code_Char_chr", "~~/src/HOL/Library/Code_Char_ord", "~~/src/HOL/Library/Code_Integer", "~~/src/HOL/Library/Efficient_Nat", "~~/src/HOL/Library/Executable_Set"(*, "Code_Prolog"*) ]; (* From ~~/src/HOL/Old_Number_Theory/ROOT.ML *) use_thys [ "~~/src/HOL/Old_Number_Theory/Fib", "~~/src/HOL/Old_Number_Theory/Factorization", "~~/src/HOL/Old_Number_Theory/Chinese", "~~/src/HOL/Old_Number_Theory/WilsonRuss", "~~/src/HOL/Old_Number_Theory/WilsonBij", "~~/src/HOL/Old_Number_Theory/Quadratic_Reciprocity", "~~/src/HOL/Old_Number_Theory/Primes", "~~/src/HOL/Old_Number_Theory/Pocklington" ]; (* From ~~/src/HOL/Algebra/ROOT.ML *) use_thys [ (*** New development, based on explicit structures ***) (* Groups *)

"~~/src/HOL/Algebra/Sylow", (* Sylow's theorem *) "~~/src/HOL/Algebra/Bij", (* Automorphism Groups *) (* Rings *) "~~/src/HOL/Algebra/Divisibility", (* Rings *)

"~~/src/HOL/Algebra/UnivPoly", (* Polynomials *) (*** Old development, based on axiomatic type classes ***) "~~/src/HOL/Algebra/abstract/Abstract", (*The ring theory*) "~~/src/HOL/Algebra/poly/Polynomial" (*The full theory*) ]; (* From ~~/src/HOL/Lattice/ROOT.ML *) use_thys [ "~~/src/HOL/Lattice/CompleteLattice" ]; (* From ~~/src/HOL/Matrix/ROOT.ML *) use_thys [ "~~/src/HOL/Matrix/Cplex" ]; (* From ~~/src/HOL/Multivariate_Analysis/ROOT.ML *) use_thys [ "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis", "~~/src/HOL/Multivariate_Analysis/Determinants" ]; (* From ~~/src/HOL/NSA/ROOT.ML *) use_thys [ "~~/src/HOL/NSA/Hypercomplex" ]; (* From ~~/src/HOL/Number_Theory/ROOT.ML *) use_thys [ "~~/src/HOL/Number_Theory/Number_Theory" ]; (* From ~~/src/HOL/Probability/ROOT.ML *) use_thys [ "~~/src/HOL/Probability/Probability" ]; (* From ~~/src/HOL/ZF/ROOT.ML *) use_thys [ "~~/src/HOL/ZF/MainZF", "~~/src/HOL/ZF/Games" ];

**Follow-Ups**:

- Previous by Date: Re: [isabelle] Non terminating function proven terminating
- Next by Date: [isabelle] ITP 2012: Call for Papers
- Previous by Thread: [isabelle] FICS 2012 Call for Papers
- 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