equal
deleted
inserted
replaced
1020 Facts are passed to $m$ as indicated by the goal's forward-chain mode, and |
1020 Facts are passed to $m$ as indicated by the goal's forward-chain mode, and |
1021 are \emph{consumed} afterwards. Thus any further $\isarkeyword{apply}$ |
1021 are \emph{consumed} afterwards. Thus any further $\isarkeyword{apply}$ |
1022 command would always work in a purely backward manner. |
1022 command would always work in a purely backward manner. |
1023 |
1023 |
1024 \item [$\isarkeyword{done}$] completes a proof script, provided that the |
1024 \item [$\isarkeyword{done}$] completes a proof script, provided that the |
1025 current goal state is solved completely. |
1025 current goal state is already solved completely. Note that actual |
1026 |
1026 structured proof commands (e.g.\ ``$\DOT$'' or $\SORRY$) may be used to |
1027 Note that actual structured proof commands (e.g.\ ``$\DOT$'', $\SORRY$) may |
1027 conclude proof scripts as well. |
1028 be used to conclude proof scripts as well. |
|
1029 |
1028 |
1030 \item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in |
1029 \item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in |
1031 terminal position. Basically, this simulates a multi-step tactic script for |
1030 terminal position. Basically, this simulates a multi-step tactic script for |
1032 $\QEDNAME$, but may be given anywhere within the proof body. |
1031 $\QEDNAME$, but may be given anywhere within the proof body. |
1033 |
1032 |