# HG changeset patch
# User nipkow
# Date 1440426340 -7200
# Node ID 6890d5875bc7d09ac52a3c6bc10f0c4ec96e9115
# Parent  40a0a40771268733235e36b24782606f669a4c25
typos

diff -r 40a0a4077126 -r 6890d5875bc7 src/Doc/Prog_Prove/Isar.thy
--- 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}