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