summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 24 May 2000 18:19:04 +0200 | |

changeset 8947 | 971aedd340e4 |

parent 8946 | 40e06237934c |

child 8948 | b797cfa3548d |

tuned;

--- a/doc-src/IsarRef/pure.tex Wed May 24 18:04:20 2000 +0200 +++ b/doc-src/IsarRef/pure.tex Wed May 24 18:19:04 2000 +0200 @@ -1022,10 +1022,9 @@ command would always work in a purely backward manner. \item [$\isarkeyword{done}$] completes a proof script, provided that the - current goal state is solved completely. - - Note that actual structured proof commands (e.g.\ ``$\DOT$'', $\SORRY$) may - be used to conclude proof scripts as well. + current goal state is already solved completely. Note that actual + structured proof commands (e.g.\ ``$\DOT$'' or $\SORRY$) may be used to + conclude proof scripts as well. \item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in terminal position. Basically, this simulates a multi-step tactic script for