The text_formalization directory is the main directory of the project.

The text_formalization/ directory contains Hol-light files for the formalization of
the text part of the Flyspeck project. It is structured along the lines of the .tex document "flypaper.tex" (Sphere Packings - a blueprint for formal proofs)

The subdirectory structure is as follows (in logical order)

The Multivariate/flyspeck.ml file is needed before any of the files in these directories.

X- build/ files related to building the project as a whole

X- general/  general definitions and tactics.
   This file contains crucial files giving the statement of the kepler conjecture.
   See general/audit_formal_proof.hl for a summary of files references in the 
   publication "A Formal Proof of the Kepler Conjecture"
   See general/the_kepler_conjecture.hl for the proved kepler conjecture.
   See general/the_main_statement.hl for the reduced form of the main statement that avoids
     the linear programming and nonlinear inequality parts of the proof.
X- nonlinear/  a list of nonlinear inequalities that are used in the text part of the proof
    See nonlinear/mk_all_ineq.hl for the code that generates the theorem
    |- the_nonlinear_inequalities
X- jordan/ some old material from the formal proof of the Jordan curve theorem.
X- leg/  lemmas in elementary geometry

Then the individual chapters follow.
1- trigonometry/  
2- volume/
3- hypermap/
4- fan/
5- packing/
6- local/
7- tame/ 

The files build/build.hl and build/strictbuild.hl go through the build sequence.
(The file build/strictbuild.hl goes through the build much more cautiously with greater
 error reporting.  The file build.hl does the ordinary everyday build.)

X- logs/ some historical logs of changes and project issues.