arith           Associativity and commutativity of unary addition
ccc             Cartesian-closed categories [incomplete]
church-rosser   The Church-Rosser theorem for untyped lambda-calculus
compile		Various compilers starting from Mini-ML
cpsocc          CPS conversion and stack-based machines [in progress]
cut-elim	Cut elimination for intuitionistic and classical logic
fol             Simple theorems in first-order logic
guide           Examples from Users' Guide
handbook        Examples from article in Handbook of Automated Reasoning
incll		Meta-interpreter for int. non-commutative linear logic
kolm		Kolmogorov translation from classical to intuitionistic logic
lp		Logic programming, uniform derivations
lp-horn		Horn fragment of logic program
mini-ml		Mini-ml, type preservation and related theorems
polylam		Polymorphic lambda-calculus
prop-calc       Natural deduction and Hilbert propositional calculus