# HG changeset patch
# User wenzelm
# Date 970686310 -7200
# Node ID 473807a5a43659bd7415cd5d07d6d8a50119e9be
# Parent  631628d6dd031d80ecc6a40da60178656e3271a0
improved @;

diff -r 631628d6dd03 -r 473807a5a436 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Wed Oct 04 20:57:32 2000 +0200
+++ b/doc-src/IsarRef/syntax.tex	Wed Oct 04 21:05:10 2000 +0200
@@ -67,7 +67,7 @@
   quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
   sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~  %$
    \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~
-   \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \mathtt{\at} ~|~ \\
+   \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~ \\
   & & \verb,^, ~|~ \verb,_, ~|~ \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\
   symbol & = & {\forall} ~|~ {\exists} ~|~ \dots
 \end{matharray}