Section 2.7.2 Definition 2.5
Otherwise, i.e., if \omega |/= P, we say that P is false at \omega.

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 11.4.6:
The unsound proof sketch on page 338 is incorrect. It should have been an unsound proof of 

v^2+w^2=r^2 | sv>=0 |- [v'=w,w'=-v,s'=5](v^2+w^2=r^2 | sv>=0)

The derivation is also missing [s':=5]. Either way, the example is demonstrating why it would be unsound to use disjunctions of differentials, because v^2+w^2=r^2 | sv>=0 does not always stay true when the right disjunct sv>=0 is true initially but the left disjunct v^2+w^2=r^2 is inductive.

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.

Section 12.4, page 380, Lemma 12.4: differential auxiliaries
The monotonicity property for the existential quantifier in the right premise with existsR and cut can be derived in different ways. The easiest way is with a cut of \exists y G and then use existsL followed by existsR to select the same variable y as witness again.

Section 12.4, page 381, Example 12.4:
Left branch should be "x!=0 <-> \exists y xy=1" instead of "x>0 <-> \exists y xy=1".

Section 12.7 page 382, Example 12.7
The right branch of the proof should have x'=-x-1 instead of x'=-x. And its top formula should have been -x*y^2 - y^2 + 2x*y*y/2 + 2y*y/2 >=0.

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 15.4 page 475:
Thus, for the formula [a*]P, Demon already has a winning strategy if he only has a strategy that is not losing by preventing !P indefinitely, because Angel eventually has to stop repeating anyhow and will then end up in a state satisfying P, which makes her lose.

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

Section 19 Example 19.3 page 570:
The top-most proof step with the <?> axiom leads to the premise (x=0 & x=x^+ & -cv=v^+) | (x!=0 & x=x^+ & v=v^+)
instead of the indicated implications.

Section 19 Example 19.6 page 573:
The top-most proof step with the <?> axiom leads to the premise (x=0 & x=x^+ & -cv=v^+) | (x!=0 & x=x^+ & v=v^+)
instead of the indicated implications.
Equation (19.7) should, thus, also read
(x=0 & x=x^+ & -cv=v^+) | (x!=0 & x=x^+ & v=v^+)

Section 20.4 page 591 before Theorem 20.2:
The text should be about equation ax^2+bx+c=0 instead of leaving out the c.

Section 20.4 page 596:
The 8a^3 in the last paragraph should be deleted.

Section 20.4 page 598 Example 20.6:
The signs of the square root expressions plugged into -x<=0 have been flipped too early. The first virtual substitution was meant of (-x<=0) for square root expression (-b+(b^2-4ac)^0.5)/(2a) whose intermediate step is (b-(b^2-4ac)^0.5)/(2a)<=0.
The second virtual substitution was meant of (-x>=0) for square root expression (-b-(b^2-4ac)^0.5)/(2a) whose intermediate step is (b+(b^2-4ac)^0.5)/(2a)<=0.

Section 20.7 page 601 Definition 20.4:
As in the text, the vanishing ideal I(V) consists of all polynomials that are zero on all of V. The definition should be:
I(V) := {f : f(x)=0 for all x\in V}

Section 21.5 page 621 Example 21.3:
the root 0 that results from considering the linear atomic formula -x<=0.