Errata

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.

1. Page 17, line 4: correct spelling is "compatibility".

2. Page 19, lines 2-3: The type of the expression (X :: nil) :: nil should be (list (list A)) rather than (list A).

3. Page 54, Figure 2.6: Two lines in that figure should be changed as follow.  

   1. "trans q2 (a::nil) q1"    ->    "trans q2 (a::nil) q2"

   2. "trans q3 (b::nil) q1"    ->    "trans q3 (b::nil) q3"

4. Page 59: the last clause defining prv is wrong.  It should read as follows:

prv Gamma Delta :-

      memb_and_rest (A ==> B) Delta Delta’,

      prv (A :: Gammma) (B :: Delta’).

5. Page 181, line 3, third character: The term (h a) should be (f a).

6. Page 210: The last reference should be ``(Nipkow 1993)'' and not ``Nipkow (1993)''.

7. 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

   1.   tr (dn b T) empty.   tr (dn b T) (tr (up b a) empty). 

8. 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 15 May 2023.