Errata
First Printing (1996)
The following Postscript file contains the corrections displayed
above: Errata.ps.
The following pages contain corrections to the first printing,
and are incorporated in the second printing:
Page028.ps
Page069.ps
Page136.ps
Page150.ps
Page160.ps
Page251.ps
Page255.ps.
First and Second Printing
The following are problems found in the second printing; they
are also present in the first printing.
 Page 71:
 Following the method pred in the first definition
of zero, there is a missing comma.
 Thanks to Gary T. Leavens.

 Page 137:
 Rule (Red Select): the third premise (xj
not in dom(S')) is simply redundant. (This redundancy
is inconsistent with the formulation of rule (Red Let).)
 Thanks to Gary T. Leavens.

 Page 146:
 The last two lines of section 11.3.2 should read:

 p1.mv_x(3); p1.x = 0
p2.mv_x(3); p2.x = 0

 Thanks to Jason M. Smith.
Second Printing (1998)
 Page 136:
 Rule (Stack x): the third premise (forall i
in 1..n) is spurious and should be ignored.
 Thanks to Gary T. Leavens.

Last updated April 27, 2000.