diff --git a/src/Lists.lagda b/src/Lists.lagda
index 4f543f85..1a5dfd1d 100644
--- a/src/Lists.lagda
+++ b/src/Lists.lagda
@@ -872,6 +872,7 @@ Do we also have the following?
 
 If so, prove; if not, explain why.
 
+
 ## Standard Library
 
 Definitions similar to those in this chapter can be found in the standard library.
diff --git a/src/Preface.lagda b/src/Preface.lagda
index 8cf1b6b0..c29809d7 100644
--- a/src/Preface.lagda
+++ b/src/Preface.lagda
@@ -28,7 +28,8 @@ an excellent time to comment on the first part.
 Since 2013, I have taught a course on Types and Semantics for
 Programming Languages to fourth-year undergraduates and masters
 students at the University of Edinburgh.  That course is not based on
-TAPL, but on Pierce's subsequent textbook, [Software Foundations][sf],
+the excellent [Types and Programming Languages][tapl] by Benjamin
+Pierce, but on Pierce's subsequent textbook, [Software Foundations][sf],
 written in collaboration with others and based on Coq.  I am convinced
 of Pierce's claim that basing a course around a proof assistant aids
 learning, as summarised in his ICFP Keynote, [Lambda, The Ultimate