This directory contains the Elf source which implements the
proof of the Church-Rosser theorem for the untyped lambda-calculus
under beta-reduction using the method of parallel reduction.
The proof (due to Tait and Martin-L"of) and this Elf code
is described in the following report.

 Frank Pfenning. A proof of the Church-Rosser theorem and its representation in
 a logical framework. Technical Report CMU-CS-92-186, Carnegie Mellon
 University, Pittsburgh, Pennsylvania, September 1992.

The file examples.quy contains the examples given in the report.
The other files are described in the file load.sml.

NOTE: The example queries require version 0.2c or newer of Elf to correctly
interpret queries of the form  ?- M : A.