[lambda] full version of subtree_equiv_lemma (agree_upto_lemma)

examples/lambda/barendregt/README.md

@@ -0,0 +1,44 @@
+chap2Script.sml :
+               mechanisation of chapter 2 of Hankin's "Lambda calculi:
+               a guide for computer scientists"
+
+chap3Script.sml :
+               mechanisation of much of chapter 3 of Hankin with bits
+               of Barendregt's chapter 3 thrown in too
+
+chap11_1Script.sml :
+               mechanisation of section 11.1 from Barendregt's "The
+               lambda calculus: its syntax and semantics"
+
+term_posnsScript.sml :
+               establishes a type for labelling reductions, and
+               positions within terms more generally
+
+finite_developmentsScript.sml :
+               Barendregt's proof of the finite-ness of developments
+               (section 11.2), mechanising this notion as well as that
+               of residuals.
+
+standardisationScript.sml :
+               Barendregt's proof of the standardisation theorem, from
+               section 11.4.
+
+preltermScript.sml ltermScript.sml :
+               script files that establish the type of lambda calculus
+               terms with labelled redexes.  Called $\Lambda'$ in
+               Barendregt.
+
+                    ------------------------------
+
+These files are behind the papers:
+
+  "Mechanising Hankin and Barendregt using the Gordon-Melham axioms"
+  Michael Norrish
+  Proceedings of the Merlin 2003 Workshop
+
+and
+
+  "Mechanising \lambda-calculus using a classical first order theory
+   of terms with permutations"
+  Michael Norrish
+  In "Higher Order and Symbolic Computation", 19:169-195, 2006.