The source files

Download the file NT.tar.gz. The command

tar -xzf NT.tar.gz

will unwrap this to a folder named NumberTheory. Everything should compile in Isabelle2004 as long as the HOL-Complex library is loaded.

To run the complete session in stand-alone mode, from just outside the folder type

isatool usedir HOL-Complex NumberTheory

To build the complete session in stand-alone mode, from inside the folder type

isatool usedir -b HOL-Complex NumberTheory

It takes about 7.5 minutes on my Thinkpad T40.

If you use Isabelle in interactive mode, you either need to put everything in a flat directory, or do the following trick

Run Isabelle: "Isabelle -l HOL-Complex"
Load "AddPath.thy", use it, and then retract it; that adds all the requisite paths to the theory loader.
Load "PrimeNumberTheorem.thy" and "use" it.