tuned markup
authornoschinl
Thu Oct 13 13:49:55 2011 +0200 (2011-10-13 ago)
changeset 451355ba2f065c6f7
parent 45134 9b02f6665fc8
child 45136 2afb928c71ca
tuned markup
doc-src/IsarRef/Thy/Proof.thy
doc-src/IsarRef/Thy/document/Proof.tex
     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
     2.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Thu Oct 13 11:45:33 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Thu Oct 13 13:49:55 2011 +0200
     2.3 @@ -902,7 +902,7 @@
     2.4    occurrences of \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} by \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}.
     2.5    
     2.6    \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
     2.7 -  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
     2.8 +  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
     2.9    backtracking across both methods.  Debugging an unsuccessful
    2.10    \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
    2.11    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