# HG changeset patch
# User nipkow
# Date 1491241277 -7200
# Node ID ac9391e04ef2f59b64e5b5f821b93641fe615b31
# Parent  65dd93a9f5b8ce0556be42b9368ae193f83f01fc# Parent  66b8309674256311cc3ad8c26a73a255b1714e26
merged

diff -r 65dd93a9f5b8 -r ac9391e04ef2 src/Doc/Prog_Prove/Isar.thy
--- a/src/Doc/Prog_Prove/Isar.thy	Mon Apr 03 19:32:16 2017 +0200
+++ b/src/Doc/Prog_Prove/Isar.thy	Mon Apr 03 19:41:17 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}.