Section 6.3:
The derivation of rule \forall\forallL from rule \forallL uses a contraction argument derived by a cut, which (as in KeYmaera X) needs sequents to consist of lists of formulas. The textbook considers sequents consisting of finite sets of formulas (Definition 6.1) and, thus, the same formula cannot occur repeatedly in the antecedent. Hence, the derivation of rule \forall\forallL needs a cut with \forall y p(y) and, instead of id, renaming (or \forallL,\existsR) to complete the proof. Thanks to Peter Schmitt for noticing this mistake.
Section 7.4:
The funny abbreviation x''.. in section 7.4 was meant to abbreviate
{x'=v,v'=-g&x>=0} including the evolution domain constraint x>=0.
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".