What programing language Thomas Hales used in 1998 to prove Kepler’s conjecture?

Question

Mathematicians have been studying sphere packings since at least 1611, when Johannes Kepler conjectured that the densest way to pack together equal-sized spheres in space is the familiar pyramidal piling of oranges seen in grocery stores. Despite the problem’s seeming simplicity, it was not settled until 1998, when Thomas Hales finally proved Kepler’s conjecture in 250 pages of mathematical arguments combined with mammoth computer calculations (3 gigabytes of computer programs, data and results).

What programing language Thomas Hales used in 1998 to prove Kepler’s conjecture?

Answer 1

The code that you are looking for is pointed to in Hales's paper Sphere packings I, but the link given therein is no longer valid; the currently valid link is on GitHub and, in Hales's own words, is a combination of C++, Java and Mathematica.

The answer given by Raymond Manzoni is not correct: he refers to a later project, in which Hales used different programming languages to formally check the validity of his original proof

Answer 2

Warning As pointed by Alex M. This answer concerns a revision of the project and not the $1998$ version (sorry for that...)

Details of the software environment used are in Hales' "A formal proof of the Kepler conjecture" paper (while the Ams paper/book is here) :

"The code and documentation for the Flyspeck project are available at a Google code repository devoted to the project 7. The parts of the project that have been carried out in Isabelle are available from the Archive of Formal Proofs ( afp.sf.net ). Other required software tools are Subversion (for interactions with the code repository), Isabelle/HOL 37, HOL Light 21, OCaml (the implementation language of HOL Light), the CamlP5 preprocessor (for a syntax extension to OCaml for parsing of mathematical terms), and GLPK (for linear programming) 8."