The files in this directory, 
Spi_Abadi_Gordon.thy, Spi_Huttel.thy, Spi_Paper.thy
come from 

Marino Miculan - Dept Math Compu Sci, University of Udine
miculan@dimi.uniud.it      http://www.dimi.uniud.it/miculan/


Look at the archive enclosed - thanks to Temesghen (who is reading in CC) that
provided me the latest versions.
Short description of the files:

1. Spi_Abadi_Gordon.thy :
  Encoding of spi-calculus as in the original paper by Abadi and Gordon.
  It should work on an earlier verison of Nominal Package on Isabelle 2005.
2. Spi_Huttel.thy :  As above with some ideas from the Huttel's paper.
3. Spi_Paper :  Latest version, described in the CiE 2008 paper.  Contains
  hedged bisimulation, framed bisimulation and two example applications.
  Examples come in two versions: proof sketches (with "sorry"s) and
  complete (without "sorry"s).

Feel free to contact Teme in case you need any explanation about these files.