instructions for running these files for Isabelle 2005 under PolyML-5

This was actually done on PolyML-5.6

Obtain the code for Isabelle2005-for-PolyML-5.6 (which is Isabelle2005,
slightly modified), from
http://users.cecs.anu.edu.au/~jeremy/isabelle/Isabelle2005-for-PolyML-5.6.tar.gz	
Get to the directory Isabelle2005-for-PolyML-5.6
(on my machine it is located at /home/users/jeremy/Isabelle2005-for-PolyML-5.6
so modify what follows accordingly)

That directory has a file called INSTALL which describes how to build
Isabelle/HOL and store it for use.

It also describes, in general terms how to run HOL.

Specifically, to run these files
you will need files in this directory, in ../gen, ../pmgms, ../seqms
You will find these in http://users.cecs.anu.edu.au/~jeremy/isabelle/2005/
Note that some of the directories also have a tar file containing the
(other) contents of that directory

Assume these are located at
/home/users/jeremy/isabelle/2005/{gen,pmgms,seqms,bimbo-dunn}
you would need to modify what follows accordingly

export ISABELLE_HOME_USER=/home/users/jeremy/isabelle
export ISABELLE_HOME=/home/users/jeremy/Isabelle2005-for-PolyML-5.6

get into the directory where the relevant files are located, eg
cd /home/users/jeremy/isabelle/2005/bimbo-dunn

poly # this should start PolyML 5.6
PolyML.SaveState.loadState
  "/home/users/jeremy/Isabelle2005-for-PolyML-5.6/heaps/HOL" ;

PolyML.use "ROOT.ML" ;
(* ths first of the following commands will take some time to build
  necessary lemmas about derivability and multisets *)
ulri 1 ; (* for cut-admissibility of LR->, LRt-> *)
usb 1 ; (* for contraction- and cut-admissibility of [LR->], [LRt->] *)
ulti 1 ; (* for cut-admissibility of the consecution calculi *)
upi 1 ; (* for the lemma concerning the pi transformation *)
utau 1 ; (* for the lemmas concerning the tau transformation *)