On Mon, 1 Dec 2008, Florian Haftmann wrote: > The switch to hg makes it possible to adapt some file locations (file > names) in the Isabelle distribution which have evolved over time but do > not fit to the logical structure of the distribution any longer, > according to the following table: > > src/Provers/* ~> src/Tools/* > src/Pure/Tools/* ~> src/Tools/* > > src/HOL/arith_data.ML ~> src/HOL/Tools > src/HOL/hologic.ML ~> src/HOL/Tools > src/HOL/simpdata.ML ~> src/HOL/Tools
I cannot really say much about HOL, you know better about its logical structure. Concerning src/Provers, src/Tools, src/Pure/Tools: * The distinction of src/Provers and src/Tools is mostly nostalgic, so Provers should go into Tools. For quite some time, we have already followed the convention of putting new things in src/Tools. * The role of src/Pure/Tools is still unclear. The difference is that these are actually loaded into the Pure image, and all its contributing sources should be in src/Pure. I would say we leave src/Pure/Tools unchanged for now until we get a better idea. BTW, moving files will also affect manuals. In the newer ones (isar-ref, system, implementation) I have already used the @{file} document antiquotation to get a statically checked references to the Isabelle file space. Makarius