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