
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}




