# HG changeset patch
# User wenzelm
# Date 947069867 -3600
# Node ID ae555dd9585b9d6889e0e1e7f9a5fea02d723041
# Parent  6186ee807f2ea3829a4b62944216b1448a3490b1
proof markup: any mode;

diff -r 6186ee807f2e -r ae555dd9585b doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Wed Jan 05 11:56:04 2000 +0100
+++ b/doc-src/IsarRef/pure.tex	Wed Jan 05 11:57:47 2000 +0100
@@ -447,11 +447,11 @@
 \indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect}
 \indexisarcmd{txt}\indexisarcmd{txt-raw}
 \begin{matharray}{rcl}
-  \isarcmd{sect} & : & \isartrans{proof(state)}{proof(state)} \\
-  \isarcmd{subsect} & : & \isartrans{proof(state)}{proof(state)} \\
-  \isarcmd{subsubsect} & : & \isartrans{proof(state)}{proof(state)} \\
-  \isarcmd{txt} & : & \isartrans{proof(state)}{proof(state)} \\
-  \isarcmd{txt_raw} & : & \isartrans{proof(state)}{proof(state)} \\
+  \isarcmd{sect} & : & \isartrans{proof}{proof} \\
+  \isarcmd{subsect} & : & \isartrans{proof}{proof} \\
+  \isarcmd{subsubsect} & : & \isartrans{proof}{proof} \\
+  \isarcmd{txt} & : & \isartrans{proof}{proof} \\
+  \isarcmd{txt_raw} & : & \isartrans{proof}{proof} \\
 \end{matharray}
 
 These markup commands for proof mode closely correspond to the ones of theory