14, -10: add "where" at the end of the line
14, -9: replace "map_list" by "map" (H. Butterworth)
14, -8: replace "map_list" by "map", "x21.0" by "x" and "x22.0" by "xs" (H. Butterworth)
15, 2: replace "now" by "not" (Qian Hong)
40, 6: replace "were" by "where" (A. Gacek)
51, 17: replace "star r'" by "star' r" (A. Butterfield)
pages 65 and 66: replace all occurrences of identifiers "even" and "Isar.even" by "evn" (A. Martini)
78, Fig. 7.1: in rule IfFalse exchange "c1" and "c2" (F. Regensburger)
78, -6: replace "s' " by "t " (F. Regensburger)
93, 16: replace "S :: nat => com " by "S :: nat => state" (C. Richardson)
130, -3: replace "the level of the information source a, but lower than or equal to l " by "both the level of the information source a and the level l " (L. Skorstengaard)
145, -10: replace "each each" by "each" (L. Panny)
152, -5: replace "have show" by "have to show" (F. Regensburger)
166, -5: replace "x" by "X" (A. Schlichtkrull)
168, 2: replace the proof text by "By the previous lemma it follows that gen c ⊆ gen w ⊆ L w X and thus that L c (L w X) = gen c ∪ (L w X - kill c) ⊆ L w X" (L. Skorstengaard)
169, 7: replace "(c,s1) => t2" by "(c,t1) => t2" (L. Skorstengaard)
176, -4: replace "until" by "until not" (N. Yamamoto)
225, -5: replace "ACom.map_acom" by "map_acom"
237, 16: replace "oder" by "order" (L. Skorstengaard)
241, 18: replace "ACom.map_acom" by "map_acom"
241, 22: replace second "φ a1" by "φ ai " (L. Skorstengaard)
242, -5: replace "13.7" by "13.3" (L. Panny)
243, -10: replace "searches" by "searches for" (A. Schlichtkrull)
261, 12: replace "that that" by "that" (L. Skorstengaard)