# HG changeset patch # User wenzelm # Date 1454852176 -3600 # Node ID 3d86222b4a941aa7a5c38769a4a3fa7e03fd760a # Parent 0e0d147b31a39cb3a59267d79b2c7c232d636ebd clarified old forms; diff -r 0e0d147b31a3 -r 3d86222b4a94 src/Doc/Isar_Ref/Proof.thy --- a/src/Doc/Isar_Ref/Proof.thy Sat Feb 06 19:26:02 2016 +0100 +++ b/src/Doc/Isar_Ref/Proof.thy Sun Feb 07 14:36:16 2016 +0100 @@ -441,14 +441,10 @@ warning beforehand. Watch out for the following message: @{verbatim [display] \Local statement fails to refine any pending goal\} - \<^descr> @{command "hence"} abbreviates ``@{command "then"}~@{command "have"}'', - i.e.\ claims a local goal to be proven by forward chaining the current - facts. Note that @{command "hence"} is also equivalent to ``@{command - "from"}~\this\~@{command "have"}''. - - \<^descr> @{command "thus"} abbreviates ``@{command "then"}~@{command "show"}''. - Note that @{command "thus"} is also equivalent to ``@{command - "from"}~\this\~@{command "show"}''. + \<^descr> @{command "hence"} expands to ``@{command "then"}~@{command "have"}'' and + @{command "thus"} expands to ``@{command "then"}~@{command "show"}''. These + conflations are left-over from early history of Isar. The expanded syntax is + more orthogonal and improves readability and maintainability of proofs. \<^descr> @{command "print_statement"}~\a\ prints facts from the current theory or proof context in long statement form, according to the syntax for @{command @@ -682,11 +678,11 @@ forward chaining are passed if so indicated by \proof(chain)\ mode. \<^descr> @{command "qed"}~\m\<^sub>2\ refines any remaining goals by proof method \m\<^sub>2\ - and concludes the sub-proof by assumption. If the goal had been \show\ (or - \thus\), some pending sub-goal is solved as well by the rule resulting from - the result \<^emph>\exported\ into the enclosing goal context. Thus \qed\ may fail - for two reasons: either \m\<^sub>2\ fails, or the resulting rule does not fit to - any pending goal\<^footnote>\This includes any additional ``strong'' assumptions as + and concludes the sub-proof by assumption. If the goal had been \show\, some + pending sub-goal is solved as well by the rule resulting from the result + \<^emph>\exported\ into the enclosing goal context. Thus \qed\ may fail for two + reasons: either \m\<^sub>2\ fails, or the resulting rule does not fit to any + pending goal\<^footnote>\This includes any additional ``strong'' assumptions as introduced by @{command "assume"}.\ of the enclosing context. Debugging such a situation might involve temporarily changing @{command "show"} into @{command "have"}, or weakening the local context by replacing occurrences diff -r 0e0d147b31a3 -r 3d86222b4a94 src/Doc/Isar_Ref/Quick_Reference.thy --- a/src/Doc/Isar_Ref/Quick_Reference.thy Sat Feb 06 19:26:02 2016 +0100 +++ b/src/Doc/Isar_Ref/Quick_Reference.thy Sun Feb 07 14:36:16 2016 +0100 @@ -57,13 +57,9 @@ @{command "proof"}~\m\<^sub>1\~@{command "qed"}~\m\<^sub>2\ \\ @{command ".."} & \\\ & @{command "by"}~\standard\ \\ @{command "."} & \\\ & @{command "by"}~\this\ \\ - @{command "hence"} & \\\ & @{command "then"}~@{command "have"} \\ - @{command "thus"} & \\\ & @{command "then"}~@{command "show"} \\ @{command "from"}~\a\ & \\\ & @{command "note"}~\a\~@{command "then"} \\ @{command "with"}~\a\ & \\\ & @{command "from"}~\a \ this\ \\ @{command "from"}~\this\ & \\\ & @{command "then"} \\ - @{command "from"}~\this\~@{command "have"} & \\\ & @{command "hence"} \\ - @{command "from"}~\this\~@{command "show"} & \\\ & @{command "thus"} \\ \end{tabular} \