# 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 \this\ is the theorem @{term "p t\<^sub>1 t\<^sub>2"} then ``\...\'' stands for \t\<^sub>2\. \item[``\.\''] (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{\t\<^sub>1 = t\<^sub>n\}, \isakeyword{show} \"t\<^sub>1 = t\<^sub>n"\ states the theorem explicitly, and ``\.\'' proves the theorem with the result of \isakeyword{finally}.