# HG changeset patch
# User wenzelm
# Date 959185144 -7200
# Node ID 971aedd340e477aa39784e8f9caf44686ebcdfda
# Parent  40e06237934ce17c22f99f8ec37eda2e2eb3470e
tuned;

diff -r 40e06237934c -r 971aedd340e4 doc-src/IsarRef/pure.tex
--- 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