diff --git a/examples/lambda/barendregt/README.md b/examples/lambda/barendregt/README.md
deleted file mode 100644
index ac295bf569..0000000000
--- a/examples/lambda/barendregt/README.md
+++ /dev/null
@@ -1,44 +0,0 @@
-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.