Mon, 24 Aug 2015 16:25:40 +0200
changeset 61013 6890d5875bc7
parent 61012 40a0a4077126
child 61020 0be2726382d9
--- 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"}}.
-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 @@
 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}.