--- a/src/Doc/Prog_Prove/Isar.thy Mon Aug 24 16:19:47 2015 +0200
+++ b/src/Doc/Prog_Prove/Isar.thy Mon Aug 24 16:25:40 2015 +0200
@@ -1068,7 +1068,7 @@
The form of the @{text IH} shows us that internally the lemma was expanded as explained
above: \noquotes{@{prop[source]"ev x \<Longrightarrow> x = Suc m \<Longrightarrow> \<not> ev m"}}.
\item
-The goal @{prop"\<not> ev (Suc n)"} may suprise. The expanded version of the lemma
+The goal @{prop"\<not> ev (Suc n)"} may surprise. The expanded version of the lemma
would suggest that we have a \isacom{fix} @{text m} \isacom{assume} @{prop"Suc(Suc n) = Suc m"}
and need to show @{prop"\<not> ev m"}. What happened is that Isabelle immediately
simplified @{prop"Suc(Suc n) = Suc m"} to @{prop"Suc n = m"} and could then eliminate
@@ -1104,7 +1104,7 @@
\begin{exercise}
Give a structured proof of @{prop "\<not> ev(Suc(Suc(Suc 0)))"}
by rule inversions. If there are no cases to be proved you can close
-a proof immediateley with \isacom{qed}.
+a proof immediately with \isacom{qed}.
\end{exercise}
\begin{exercise}