--- a/doc-src/IsarRef/Thy/document/syntax.tex Thu May 08 22:17:37 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/syntax.tex Thu May 08 22:20:33 2008 +0200
@@ -510,16 +510,16 @@
\indexdef{}{antiquotation}{abbrev}\mbox{\isa{abbrev}} & : & \isarantiq \\
\indexdef{}{antiquotation}{typeof}\mbox{\isa{typeof}} & : & \isarantiq \\
\indexdef{}{antiquotation}{typ}\mbox{\isa{typ}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{thm-style}\mbox{\isa{thm{\isacharunderscore}style}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{term-style}\mbox{\isa{term{\isacharunderscore}style}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{thm\_style}\mbox{\isa{thm{\isacharunderscore}style}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{term\_style}\mbox{\isa{term{\isacharunderscore}style}} & : & \isarantiq \\
\indexdef{}{antiquotation}{text}\mbox{\isa{text}} & : & \isarantiq \\
\indexdef{}{antiquotation}{goals}\mbox{\isa{goals}} & : & \isarantiq \\
\indexdef{}{antiquotation}{subgoals}\mbox{\isa{subgoals}} & : & \isarantiq \\
\indexdef{}{antiquotation}{prf}\mbox{\isa{prf}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{full-prf}\mbox{\isa{full{\isacharunderscore}prf}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{full\_prf}\mbox{\isa{full{\isacharunderscore}prf}} & : & \isarantiq \\
\indexdef{}{antiquotation}{ML}\mbox{\isa{ML}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{ML-type}\mbox{\isa{ML{\isacharunderscore}type}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{ML-struct}\mbox{\isa{ML{\isacharunderscore}struct}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{ML\_type}\mbox{\isa{ML{\isacharunderscore}type}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{ML\_struct}\mbox{\isa{ML{\isacharunderscore}struct}} & : & \isarantiq \\
\end{matharray}
The text body of formal comments (see also \secref{sec:comments})
@@ -579,7 +579,7 @@
\item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints theorems
\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}. Note that attribute specifications
may be included as well (see also \secref{sec:syn-att}); the
- \indexref{}{attribute}{no-vars}\mbox{\isa{no{\isacharunderscore}vars}} rule (see \secref{sec:misc-meth-att}) would
+ \indexref{}{attribute}{no\_vars}\mbox{\isa{no{\isacharunderscore}vars}} rule (see \secref{sec:misc-meth-att}) would
be particularly useful to suppress printing of schematic variables.
\item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}}] prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.