merged
authornipkow
Mon Apr 03 19:41:17 2017 +0200 (2017-04-03)
changeset 65353ac9391e04ef2
parent 65351 65dd93a9f5b8
parent 65352 66b830967425
child 65354 4ff2ba82d668
merged
     1.1 --- a/src/Doc/Prog_Prove/Isar.thy	Mon Apr 03 19:32:16 2017 +0200
     1.2 +++ b/src/Doc/Prog_Prove/Isar.thy	Mon Apr 03 19:41:17 2017 +0200
     1.3 @@ -462,7 +462,7 @@
     1.4  In general, if \<open>this\<close> is the theorem @{term "p t\<^sub>1 t\<^sub>2"} then ``\<open>...\<close>''
     1.5  stands for \<open>t\<^sub>2\<close>.
     1.6  \item[``\<open>.\<close>''] (a single dot) is a proof method that solves a goal by one of the
     1.7 -assumptions. This works because the result of \isakeyword{finally}
     1.8 +assumptions. This works here because the result of \isakeyword{finally}
     1.9  is the theorem \mbox{\<open>t\<^sub>1 = t\<^sub>n\<close>},
    1.10  \isakeyword{show} \<open>"t\<^sub>1 = t\<^sub>n"\<close> states the theorem explicitly,
    1.11  and ``\<open>.\<close>'' proves the theorem with the result of \isakeyword{finally}.