5, line -14: insert "free" before "occurrences". (Tjark Weber)
7, line 5: replace "must a ?" by "must have a ?". (Michael Ernst)
10, line 17: replace "are can" by "can". (Sara Kalvala)
23, line -12: replace "auto" by "simp" because auto can in fact prove the goal.
28, line -7: replace "differnt" by "different". (Tjark Weber)
35, line 21: replace "," by ".".
43, line 13: replace "the the" by "the". (Michael Ernst)
55, line 9: replace "a Isabelle symbol" by "an Isabelle symbol". (Michael Ernst)
67, line 4: replace "require" by "requires".
78, line 7: delete "it" in "method it in". (Wolfram Kahl)
87: line "5.11 ..." - 2: insert "the" before "$\varepsilon$-operator". (Wolfram Kahl)
101, exercise 5.16.1: replace "intro?" by "(intro conjI)?". (Michel Charpentier)
105, line 11: replace "sets" by "Sets". (Michael Ernst)
109, lines 4-5: replace "z" by "x". (Tjark Weber)
111, line 17: add double-quote (") at end of line. (Michael Ernst)
175, line -15: replace "legal use" by "legal to use". (Sara Kalvala)
This errata refers to the printed version of the Tutorial. Page and line numbers may be slightly off for the online version.