--- a/src/Doc/Prog_Prove/Isar.thy Mon Apr 03 18:05:17 2017 +0200
+++ b/src/Doc/Prog_Prove/Isar.thy Mon Apr 03 19:40:26 2017 +0200
@@ -462,7 +462,7 @@
In general, if \<open>this\<close> is the theorem @{term "p t\<^sub>1 t\<^sub>2"} then ``\<open>...\<close>''
stands for \<open>t\<^sub>2\<close>.
\item[``\<open>.\<close>''] (a single dot) is a proof method that solves a goal by one of the
-assumptions. This works because the result of \isakeyword{finally}
+assumptions. This works here because the result of \isakeyword{finally}
is the theorem \mbox{\<open>t\<^sub>1 = t\<^sub>n\<close>},
\isakeyword{show} \<open>"t\<^sub>1 = t\<^sub>n"\<close> states the theorem explicitly,
and ``\<open>.\<close>'' proves the theorem with the result of \isakeyword{finally}.