equal
deleted
inserted
replaced
64 of this at the same time. |
64 of this at the same time. |
65 \end{warn} |
65 \end{warn} |
66 *} |
66 *} |
67 |
67 |
68 |
68 |
69 section {* Lexical matters \label{sec:lex-syntax} *} |
69 section {* Lexical matters \label{sec:outer-lex} *} |
70 |
70 |
71 text {* |
71 text {* The Isabelle/Isar outer syntax provides token classes as |
72 The Isabelle/Isar outer syntax provides token classes as presented |
72 presented below; most of these coincide with the inner lexical |
73 below; most of these coincide with the inner lexical syntax as |
73 syntax as defined in \secref{sec:inner-lex}. |
74 presented in \cite{isabelle-ref}. |
|
75 |
74 |
76 \begin{matharray}{rcl} |
75 \begin{matharray}{rcl} |
77 @{syntax_def ident} & = & letter\,quasiletter^* \\ |
76 @{syntax_def ident} & = & letter\,quasiletter^* \\ |
78 @{syntax_def longident} & = & ident (\verb,.,ident)^+ \\ |
77 @{syntax_def longident} & = & ident (\verb,.,ident)^+ \\ |
79 @{syntax_def symident} & = & sym^+ ~|~ \verb,\,\verb,<,ident\verb,>, \\ |
78 @{syntax_def symident} & = & sym^+ ~|~ \verb,\,\verb,<,ident\verb,>, \\ |