The following errors in the text have been reported to the authors. We are grateful to readers for sending us errors as they find them.
- Page 17, line 4: correct spelling is "compatibility".
- Page 54, Figure 2.6: Two lines in that figure should be changed as follow.
"trans q2 (a::nil) q1" -> "trans q2 (a::nil) q2"
"trans q3 (b::nil) q1" -> "trans q3 (b::nil) q3"
- Page 181, line 3, third character: The term (h a) should be (f a).
- Page 210: The last reference should be ``(Nipkow 1993)'' and not ``Nipkow (1993)''.
- Page 268, lines 9 and 8 from the bottom: The symbol trp in both these lines should be tr, i.e. these lines should read
tr (dn b T) empty.
tr (dn b T) (tr (up b a) empty).
Page 230: The instance of an implication-left rule near the bottom is wrong. The correct form replaces all occurrences of "p" with "q". Also, the second line from the bottom should refer to the six rules displayed in Figure 9.2 (not four rules).
Last updated 12 December 2013.