diff --git a/src/Lambda.lagda b/src/Lambda.lagda
index ae77e441..a3f22df6 100644
--- a/src/Lambda.lagda
+++ b/src/Lambda.lagda
@@ -4,8 +4,8 @@ layout    : page
 permalink : /Lambda/
 ---
 
-[Parts of this chapter take their text from chapter _Stlc_ in
-book _Programming Language Foundations_ of _Software Foundations_.
+[Parts of this chapter take their text from chapter _Stlc_
+of _Software Foundations_ (_Programming Language Foundations_).
 Those parts will be revised.]
 
 The _lambda-calculus_, first published by the logician Alonzo Church in
@@ -35,7 +35,8 @@ variables, partly because such terms are easier to read and partly
 because the development is more traditional.
 
 The development in this chapter was inspired by the corresponding
-development in Chapter STLC of _Software Foundations_.  We differ by
+development in Chapter _Stlc_ of _Software Foundations_ 
+(_Programming Language Foundations_).  We differ by
 representing contexts explicitly (as lists pairing identifiers with
 types) rather than as partial maps (which take identifiers to types),
 which will corresponds better to our subsequent development of DeBruin
diff --git a/src/LambdaProp.lagda b/src/LambdaProp.lagda
index bbdb071e..7a2ca412 100644
--- a/src/LambdaProp.lagda
+++ b/src/LambdaProp.lagda
@@ -4,18 +4,20 @@ layout    : page
 permalink : /LambdaProp/
 ---
 
-[Parts of this chapter take their text from chapter StlcProp in
-_Software Foundations: Programming Language Foundations_.
+[Parts of this chapter take their text from chapter _Stlc_
+of _Software Foundations_ (_Programming Language Foundations_).
 Those parts will be revised.]
 
 This chapter develops the fundamental theory of the Simply
 Typed Lambda Calculus, particularly progress and preservation.
 
 The development in this chapter was inspired by the corresponding
-development in Chapter STLCProp of _Software Foundations_.  It will turn
+development in Chapter _StlcProp_ of _Software Foundations_
+(_Programming Language Foundations_).  It will turn
 out that one of our technical choices in the previous chapter
-(to introduce an explicit judgment `Γ ∋ x ⦂ A`) permits a somewhat
-simpler development. In particular, we can prove substitution preserves
+(to introduce an explicit judgment `Γ ∋ x ⦂ A` in place of
+treating a context as a function from identifiers to types)
+permits a simpler development. In particular, we can prove substitution preserves
 types without needing to develop a separate inductive definition of the
 `appears_free_in` relation.
 
@@ -780,6 +782,7 @@ false, give a counterexample.
 
 
 #### Exercise: 2 stars, optional (stlc_variation6)
+
 Suppose instead that we add the following new rule to the typing
 relation: