From e204041ff8dbc93fe1565bf925039a10efbb1375 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 2 Apr 2017 19:18:34 -0400
Subject: [PATCH] Tiny revisions to LambdaCalculusAndTypeSoundness

---
 LambdaCalculusAndTypeSoundness_template.v | 2 +-
 frap_book.tex                             | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/LambdaCalculusAndTypeSoundness_template.v b/LambdaCalculusAndTypeSoundness_template.v
index 3585756..1c5ab96 100644
--- a/LambdaCalculusAndTypeSoundness_template.v
+++ b/LambdaCalculusAndTypeSoundness_template.v
@@ -591,7 +591,7 @@ Module Stlc.
   Proof.
   Admitted.
 
-  Theorem safety_snazzy : forall e t, hasty $0 e t
+  Theorem safety : forall e t, hasty $0 e t
     -> invariantFor (trsys_of e) unstuck.
   Proof.
     simplify.
diff --git a/frap_book.tex b/frap_book.tex
index 0985dde..e12f142 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -2553,7 +2553,7 @@ We write $\smallstepcls{s}{\ell}{s'}$ to indicate that $s$ steps to $s'$ via zer
 
 \chapter{Lambda Calculus and Simple Type Safety}
 
-We'll now take a break from the imperative language we've been studying for the last two chapters, instead looking at a classic sort of small language that distills the essence of \emph{functional} programming\index{functional programming}.
+We'll now take a break from the imperative language we've been studying for the last three chapters, instead looking at a classic sort of small language that distills the essence of \emph{functional} programming\index{functional programming}.
 That's the language paradigm that we've been using throughout this book, as we coded executable versions of algorithms.
 Its distinctive characteristics are first, a computation style based on simplifying terms instead of running step-by-step instructions that modify state; and second, use of functions as first-class values.
 Functional programming went mainstream in the early 21st century, influencing widely adopted languages from JavaScript\index{JavaScript}, where first-class functions are routinely used as callbacks in asynchronous event processing; to Scala\index{Scala}, a hybrid language that melds functional-programming ideas with object-oriented programming for the Java platform; to Haskell\index{Haskell}, a purely functional language that has become popular with programming hobbyists and is seeing increasing adoption in industry.