# HG changeset patch
# User wenzelm
# Date 949945367 -3600
# Node ID 985c876b777ebddb2395ff630f2e79dc5aa94dc8
# Parent  e50a130ec9af00eee3d4e42ca4bee234b1d8e492
(then_)apply: prove -> prove;

diff -r e50a130ec9af -r 985c876b777e doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Mon Feb 07 18:40:40 2000 +0100
+++ b/doc-src/IsarRef/pure.tex	Mon Feb 07 18:42:47 2000 +0100
@@ -737,8 +737,8 @@
 
 \indexisarcmd{apply}\indexisarcmd{then-apply}\indexisarcmd{back}
 \begin{matharray}{rcl}
-  \isarcmd{apply}^* & : & \isartrans{proof}{proof} \\
-  \isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\
+  \isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\
+  \isarcmd{then_apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\
   \isarcmd{back}^* & : & \isartrans{proof}{proof} \\
 \end{matharray}