equal
deleted
inserted
replaced
61 \end{isamarkuptext}% |
61 \end{isamarkuptext}% |
62 \isamarkuptrue% |
62 \isamarkuptrue% |
63 % |
63 % |
64 \isamarkupsection{Proof structure% |
64 \isamarkupsection{Proof structure% |
65 } |
65 } |
|
66 \isamarkuptrue% |
|
67 % |
|
68 \isamarkupsubsection{Example proofs% |
|
69 } |
|
70 \isamarkuptrue% |
|
71 % |
|
72 \begin{isamarkuptext}% |
|
73 \begin{matharray}{rcl} |
|
74 \indexdef{}{command}{example\_proof}\hypertarget{command.example-proof}{\hyperlink{command.example-proof}{\mbox{\isa{\isacommand{example{\isacharunderscore}proof}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\ |
|
75 \end{matharray} |
|
76 |
|
77 \begin{description} |
|
78 |
|
79 \item \hyperlink{command.example-proof}{\mbox{\isa{\isacommand{example{\isacharunderscore}proof}}}} opens an empty proof body. This |
|
80 allows to experiment with Isar, without producing any persistent |
|
81 result. |
|
82 |
|
83 Structurally, this is like a vacous \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} statement |
|
84 followed by ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'', which means the |
|
85 example proof may be closed by a regular \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}, or |
|
86 discontinued by \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}. |
|
87 |
|
88 \end{description}% |
|
89 \end{isamarkuptext}% |
66 \isamarkuptrue% |
90 \isamarkuptrue% |
67 % |
91 % |
68 \isamarkupsubsection{Blocks% |
92 \isamarkupsubsection{Blocks% |
69 } |
93 } |
70 \isamarkuptrue% |
94 \isamarkuptrue% |