diff -r e877eec2b698 -r 627f369d505e src/Doc/ProgProve/Isar.thy
--- a/src/Doc/ProgProve/Isar.thy	Mon Nov 25 00:02:39 2013 +0000
+++ b/src/Doc/ProgProve/Isar.thy	Mon Nov 25 08:22:29 2013 +0100
@@ -1019,7 +1019,7 @@
 \isacom{lemma} @{text[source]"I r s t \<Longrightarrow> \<dots>"}
 \end{isabelle}
 Applying the standard form of
-rule induction in such a situation will lead to strange and typically unproveable goals.
+rule induction in such a situation will lead to strange and typically unprovable goals.
 We can easily reduce this situation to the standard one by introducing
 new variables @{text x}, @{text y}, @{text z} and reformulating the goal like this:
 \begin{isabelle}
@@ -1041,7 +1041,7 @@
 proof(induction "Suc m" arbitrary: m rule: ev.induct)
   fix n assume IH: "\<And>m. n = Suc m \<Longrightarrow> \<not> ev m"
   show "\<not> ev (Suc n)"
-  proof --"contradition"
+  proof --"contradiction"
     assume "ev(Suc n)"
     thus False
     proof cases --"rule inversion"