summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Mon, 03 Apr 2017 19:41:17 +0200 | |

changeset 65353 | ac9391e04ef2 |

parent 65351 | 65dd93a9f5b8 (current diff) |

parent 65352 | 66b830967425 (diff) |

child 65354 | 4ff2ba82d668 |

merged

--- 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}.