summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/IsarRef/Thy/Proof.thy

changeset 45135 | 5ba2f065c6f7 |

parent 45103 | a45121ffcfcb |

child 46262 | 912b42e64fde |

1.1 --- a/doc-src/IsarRef/Thy/Proof.thy Thu Oct 13 11:45:33 2011 +0200 1.2 +++ b/doc-src/IsarRef/Thy/Proof.thy Thu Oct 13 13:49:55 2011 +0200 1.3 @@ -655,7 +655,7 @@ 1.4 1.5 \item @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} is a \emph{terminal 1.6 proof}\index{proof!terminal}; it abbreviates @{command 1.7 - "proof"}~@{text "m\<^sub>1"}~@{text "qed"}~@{text "m\<^sub>2"}, but with 1.8 + "proof"}~@{text "m\<^sub>1"}~@{command "qed"}~@{text "m\<^sub>2"}, but with 1.9 backtracking across both methods. Debugging an unsuccessful 1.10 @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} command can be done by expanding its 1.11 definition; in many cases @{command "proof"}~@{text "m\<^sub>1"} (or even