Section 5.6.1 page 161 above Lemma 5.10:
... the already-established postcondition P implies the originally desired postcondition Q.
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. Likewise the text should have talked about the differential invariant v=v_0-tg instead of v=v_0=tg.
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 12.7 page 388 equation (12.9):
e_1 should have been u_1.
Section 13.12 page 415:
If, e.g., the coordinate with maximal absolute value is at most 1, then the Euclidean distance can be at most \sqrt{2}.
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".