[isabelle-dev] Directory layout

[Florian Haftmann]

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
    src/HOL/int_arith1.ML ~> src/HOL/Tools/int_arith.ML
    src/HOL/int_factor_simprocs.ML ~> src/HOL/Tools
    src/HOL/nat_simprocs.ML ~> src/HOL/Tools
    src/HOL/Real/float_syntax.ML ~> src/HOL/Tools
    src/HOL/Real/rat_arith.ML ~> src/HOL/Tools
    src/HOL/Real/real_arith.ML ~> src/HOL/Tools

    src/HOL/Library/RType.thy ~> src/HOL/Typerep.thy
    src/HOL/Library/Code_Message.thy ~> src/HOL/
    src/HOL/Library/Dense_Linear_Order.thy ~> src/HOL
    src/HOL/Library/GCD.thy ~> src/HOL
    src/HOL/Library/Order_Relation.thy ~> src/HOL
    src/HOL/Library/Parity.thy ~> src/HOL
    src/HOL/Library/Univ_Poly.thy ~> src/HOL
    src/HOL/Real/ContNotDenum.thy ~> src/HOL
    src/HOL/Real/Lubs.thy ~> src/HOL
    src/HOL/Real/PReal.thy ~> src/HOL
    src/HOL/Real/Rational.thy ~> src/HOL
    src/HOL/Real/RComplete.thy ~> src/HOL
    src/HOL/Real/RealDef.thy ~> src/HOL
    src/HOL/Real/RealPow.thy ~> src/HOL
    src/HOL/Real/Real.thy ~> src/HOL
    src/HOL/Real/RealVector.thy ~> src/HOL
    src/HOL/Complex/Complex_Main.thy ~> src/HOL
    src/HOL/Complex/Complex.thy ~> src/HOL
    src/HOL/Complex/Fundamental_Theorem_Algebra.thy ~> src/HOL
    src/HOL/Hyperreal/Deriv.thy ~> src/HOL
    src/HOL/Hyperreal/Fact.thy ~> src/HOL
    src/HOL/Hyperreal/Integration.thy ~> src/HOL
    src/HOL/Hyperreal/Lim.thy ~> src/HOL
    src/HOL/Hyperreal/Ln.thy ~> src/HOL
    src/HOL/Hyperreal/Log.thy ~> src/HOL
    src/HOL/Hyperreal/MacLaurin.thy ~> src/HOL
    src/HOL/Hyperreal/NthRoot.thy ~> src/HOL
    src/HOL/Hyperreal/SEQ.thy ~> src/HOL
    src/HOL/Hyperreal/Series.thy ~> src/HOL
    src/HOL/Hyperreal/Taylor.thy ~> src/HOL
    src/HOL/Hyperreal/Transcendental.thy ~> src/HOL

    src/HOL/Complex/ex/BigO_Complex.thy ~> src/HOL/ex
    src/HOL/Complex/ex/BinEx.thy ~> src/HOL/ex
    src/HOL/Complex/ex/Sqrt.thy ~> src/HOL/ex
    src/HOL/Complex/ex/Sqrt_Script.thy ~> src/HOL/ex
    src/HOL/Complex/ex/MIR.thy ~> src/HOL/ex
    src/HOL/Complex/ex/mirtac.ML ~> src/HOL/ex
    src/HOL/Complex/ex/ReflectedFerrack.thy ~> src/HOL/ex
    src/HOL/Complex/ex/linrtac.ML ~> src/HOL/ex

If there are no objections, I would carry out these movements this
Wednesday.

A further step will consider HOL/Library and HOL/ex;  the ideas are to
split off larger library blocks into separate directories, move
re-usable examples from HOL/ex to HOL/Library and split off pure test
examples (e.g. code generator coverage test) from HOL/ex into a separate
session.

	Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20081201/fef5ca18/attachment.sig>