# HG changeset patch
# User paulson
# Date 826043001 -3600
# Node ID 61f5410b2824b88f45119b12f44e407d36df1bb7
# Parent ad47d58ecb375a876b63cfd0923f989b4ac7a189
New documentation for example
diff -r ad47d58ecb37 -r 61f5410b2824 src/ZF/Resid/README.html
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Resid/README.html Tue Mar 05 17:23:21 1996 +0100
@@ -0,0 +1,28 @@
+
+HOL/Resid
+
+Resid -- A theory of residuals
+
+Ole Rasmussen has ported to Isabelle/ZF the Coq proofs described in the
+article
+
+
+
+@Article{huet-residual,
+ author = "{G\'erard} Huet",
+ title = "Residual Theory in $\lambda$-Calculus: A Formal
+ Development",
+ journal = JFP,
+ year = 1994,
+ volume = 4,
+ number = 3,
+ pages = "371--394"}
+
+
+See Rasmussen's report
+The Church-Rosser Theorem in Isabelle: A Proof Porting
+ Experiment.
+
+
+
+Last modified 5 March 1996