# HG changeset patch
# User nipkow
# Date 1491241226 -7200
# Node ID 66b8309674256311cc3ad8c26a73a255b1714e26
# Parent  6e47bcf7bec4b8217742ce0bee308379a364f1cf
tuned

diff -r 6e47bcf7bec4 -r 66b830967425 src/Doc/Prog_Prove/Isar.thy
--- 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}.