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 *)