# HG changeset patch
# User wenzelm
# Date 959184260 -7200
# Node ID 40e06237934ce17c22f99f8ec37eda2e2eb3470e
# Parent  17365afd950249d9fc07e6bc6c28727b24029904
"done" command;

diff -r 17365afd9502 -r 40e06237934c doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Wed May 24 13:16:01 2000 +0200
+++ b/doc-src/IsarRef/pure.tex	Wed May 24 18:04:20 2000 +0200
@@ -951,7 +951,7 @@
 tactical proof within new-style theories (to benefit from document
 preparation, for example).
 
-\indexisarcmd{apply}\indexisarcmd{apply-end}
+\indexisarcmd{apply}\indexisarcmd{done}\indexisarcmd{apply-end}
 \indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back}
 \indexisarmeth{tactic}\indexisarmeth{insert}
 \indexisarmeth{res-inst-tac}\indexisarmeth{eres-inst-tac}
@@ -959,6 +959,7 @@
 \indexisarmeth{subgoal-tac}
 \begin{matharray}{rcl}
   \isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\
+  \isarcmd{done}^* & : & \isartrans{proof(prove)}{proof(state)} \\
   \isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\
   \isarcmd{defer}^* & : & \isartrans{proof}{proof} \\
   \isarcmd{prefer}^* & : & \isartrans{proof}{proof} \\
@@ -993,6 +994,8 @@
 \begin{rail}
   'apply' method comment?
   ;
+  'done' comment?
+  ;
   applyend method comment?
   ;
   'defer' nat? comment?
@@ -1012,13 +1015,17 @@
 \begin{descr}
 \item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in initial
   position, but unlike $\PROOFNAME$ it retains ``$proof(prove)$'' mode.  Thus
-  consecutive method applications may be given just as in tactic scripts.  In
-  order to complete the proof properly, any of the actual structured proof
-  commands (e.g.\ ``$\DOT$'') has to be given eventually.
+  consecutive method applications may be given just as in tactic scripts.
   
   Facts are passed to $m$ as indicated by the goal's forward-chain mode, and
   are \emph{consumed} afterwards.  Thus any further $\isarkeyword{apply}$
   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.
 
 \item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in
   terminal position.  Basically, this simulates a multi-step tactic script for