This directory contains software and reports related to ML, LCF and Isabelle.
Directory "reports" at this ftp site contains some relevant technical reports.

**** Full contents of this directory (alphabetical order) ****

00Index		  : this file
ERRATA1.txt  	  : Errata in "ML for the Working Programmer", 1st printing
ERRATA2.txt  	  : Errata in "ML for the Working Programmer", 2nd printing
ERRATA3.txt  	  : Errata in "ML for the Working Programmer", 3rd printing
Elle-2.4.tar.gz	  : Elle Verification Environment for ML (requires Isabelle-93)
Isabelle93.tar.gz : the Isabelle-93 alpha distribution 
Isabelle92.tar.gz : the Isabelle-92 beta distribution (OBSOLETE)
answers1-5.txt.gz : answers to the exercises in the book "ML for the Working 
		  Programmer" by L Paulson (CUP, 1991), chapters 1-5
cant-ozols.ps.gz  : "A Verification Environment for ML Programs", by
		   A Cant and M A Ozols, Trusted Computer Systems Group, DSTO
coind.ps.gz 	  : "Co-induction and Co-recursion in H.O. Logic", by L Paulson
isabelle-users.90-92.gz : archive of isabelle-users email list for 1990-92
isabelle-users.93.gz :    archive of isabelle-users email list for 1993
lcf.tar.gz	  : the Cambridge LCF theorem prover; see the book "Logic and 
		    Computation" by L Paulson (CUP, 1987)
lib.dvi.gz	  : "A Selection from the Proof Libraries of Isabelle"
set-I.ps.gz	  : "Set Theory for Verification", Part I, by L Paulson
working.tar.gz	  : programs from the book "ML for the Working Programmer"


**** Contents of this directory (subject order) ****

** Isabelle and applications **

Isabelle93.tar.gz : the Isabelle-93 alpha distribution 
Isabelle92.tar.gz : the Isabelle-92 beta distribution (OBSOLETE)
Elle-2.4.tar.gz	  : Elle Verification Environment for ML, courtesy DSTO
isabelle-users.90-92.gz : archive of the isabelle-users email list

** Papers concerning Isabelle **

cant-ozols.ps.gz  : "A Verification Environment for ML Programs", by
		     A Cant and M A Ozols, Trusted Computer Systems Group, DSTO
set-I.ps.gz	  : "Set Theory for Verification", Part I, by L Paulson
coind.ps.gz 	  : "Co-induction and Co-recursion in H.O. Logic", by L Paulson
lib.dvi.gz	  : "A Selection from the Proof Libraries of Isabelle"

** ML for the Working Programmer **

answers1-5.txt.gz : answers to the exercises, chapters 1-5
ERRATA1.txt  	  : Errata in "ML for the Working Programmer", 1st printing
ERRATA2.txt  	  : Errata in "ML for the Working Programmer", 2nd printing
ERRATA3.txt  	  : Errata in "ML for the Working Programmer", 3rd printing
working.tar.gz	  : sample programs from the book


** Logic for Computable Functions (LCF) **

lcf.tar.gz	  : the Cambridge LCF theorem prover; see the book "Logic and 
		    Computation" by L Paulson (CUP, 1987)
