Section 7.7.4:
Left branch of the proof in section 7.7.4 uses [*],/\L in addition to id.
Section 12.3.2 page 372:
The last cancelled term in the second equation should be -t^2g^2 instead of +t^2g^2.
Example 12.4 in section 12.4 page 381:
Left branch should be "x!=0 <-> \exists y xy=1" instead of "x>0 <-> \exists y xy=1".
Section 17.4 Figure 17.4:
The necessary assumption x=a=1 on the left-hand side of the conclusion of the choice game should have been kept throughout the proof by replacing all occurrences of the formula "true" in the sequent proof by the original assumption "x=a=1". Additionally, the universal quantifier should have been "for all x,a" instead of just "for all x".
Section 17.4 Figure 17.5:
The necessary assumption x>=0 on the left-hand side of the conclusion of the 2-Nim-type game should have been kept throughout the proof by replacing all occurrences of the formula "true" in the sequent proof by the original assumption "x>=0".