(then_)apply: prove -> prove;
authorwenzelm
Mon, 07 Feb 2000 18:42:47 +0100
changeset 8207 985c876b777e
parent 8206 e50a130ec9af
child 8208 67d9d52b0b72
(then_)apply: prove -> prove;
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}