TO COPY MY POLYML-4.1.4 INSTALLATION AND RUN ISABELLE2005 ON IT

This was done on a computer, running Linux, with the following details:

Linux robotpc3-temp.cs.ucl.ac.uk 3.6.11-4.fc16.i686.PAE #1 SMP Tue Jan 8 21:18:14 UTC 2013 i686 i686 i386 GNU/Linux

so here are instructions for what I did 
the computer had 32-bit libraries installed.
Doing (from the directory where you unpack polyml-4.1.4.tar)
cd polyml-4.1.4/x86-linux
ldd poly
may make it clear whether you need to install them

Go to 
http://users.cecs.anu.edu.au/~jeremy/isabelle/
Download Isabelle2005.tar and polyml-4.1.4.tar	

Choose a directory to work (it's /home/users/jeremy in my own case)

Put the tar files into that directory and unpack them (tar xvf filename.tar)

In Isabelle2005/etc/settings you need to edit it by changing
/home/users/jeremy to whatever directory you have chosen to use

Then type 
/home/users/jeremy/Isabelle2005/bin/isabelle (changed as necessary).
which should start Isabelle 2005

If this works you can type 
[sym, refl, trans] ;
and it will display the text of those three theorems.

FOLLOWING IS ABOUT RUNNING CERTAIN SPECIFIC THEORIES
(and maybe out-of-date since some changes have been made to these
theories for use in my version of Isabelle2005 for PolyML-5.6)

For the specific work of the paper you need to download a lot of files from
http://users.cecs.anu.edu.au/~jeremy/isabelle/2005/gen/

Easiest to download just gen.tar and unpack it, to create a whole lot of files
in your directory (which you need to create) isabelle/2005/gen/
(or choose another directory if you like)

Get into this directory and start Isabelle as above by 
/home/users/jeremy/Isabelle2005/bin/isabelle (changed as necessary).

Then
use_thy "tripartite" ;
should run a lot of preliminary proofs then the results of the paper
(of which the last is wf_rearr_n)

[notes added later]
You need to have perl installed - which is sometimes included in a 
dafault installation of Linux, sometimes not