# HG changeset patch # User noschinl # Date 1318506595 -7200 # Node ID 5ba2f065c6f74ba5dfdc10e78d254a81a3d30ea4 # Parent 9b02f6665fc85bde39dceba3016364d27cce0f04 tuned markup diff -r 9b02f6665fc8 -r 5ba2f065c6f7 doc-src/IsarRef/Thy/Proof.thy --- a/doc-src/IsarRef/Thy/Proof.thy Thu Oct 13 11:45:33 2011 +0200 +++ b/doc-src/IsarRef/Thy/Proof.thy Thu Oct 13 13:49:55 2011 +0200 @@ -655,7 +655,7 @@ \item @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} is a \emph{terminal proof}\index{proof!terminal}; it abbreviates @{command - "proof"}~@{text "m\<^sub>1"}~@{text "qed"}~@{text "m\<^sub>2"}, but with + "proof"}~@{text "m\<^sub>1"}~@{command "qed"}~@{text "m\<^sub>2"}, but with backtracking across both methods. Debugging an unsuccessful @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} command can be done by expanding its definition; in many cases @{command "proof"}~@{text "m\<^sub>1"} (or even diff -r 9b02f6665fc8 -r 5ba2f065c6f7 doc-src/IsarRef/Thy/document/Proof.tex --- a/doc-src/IsarRef/Thy/document/Proof.tex Thu Oct 13 11:45:33 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Thu Oct 13 13:49:55 2011 +0200 @@ -902,7 +902,7 @@ occurrences of \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} by \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}. \item \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} is a \emph{terminal - proof}\index{proof!terminal}; it abbreviates \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}~\isa{{\isaliteral{22}{\isachardoublequote}}qed{\isaliteral{22}{\isachardoublequote}}}~\isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}, but with + proof}\index{proof!terminal}; it abbreviates \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}, but with backtracking across both methods. Debugging an unsuccessful \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} command can be done by expanding its definition; in many cases \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} (or even