77 nat & = & digit^+ \\ |
77 nat & = & digit^+ \\ |
78 var & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\ |
78 var & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\ |
79 typefree & = & \verb,',ident \\ |
79 typefree & = & \verb,',ident \\ |
80 typevar & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\ |
80 typevar & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\ |
81 string & = & \verb,", ~\dots~ \verb,", \\ |
81 string & = & \verb,", ~\dots~ \verb,", \\ |
82 verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\ |
82 verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\[1ex] |
83 \end{matharray} |
83 |
84 \begin{matharray}{rcl} |
84 letter & = & sletter ~|~ xletter \\ |
85 letter & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\ |
|
86 digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\ |
85 digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\ |
87 quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\ |
86 quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\ |
88 sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~ %$ |
87 sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~ %$ |
89 \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~ \\ |
88 \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~ \\ |
90 & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~ |
89 & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~ |
91 \verb,^, ~|~ \verb,_, ~|~ \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\ |
90 \verb,^, ~|~ \verb,_, ~|~ \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\ |
92 symbol & = & {\forall} ~|~ {\exists} ~|~ {\land} ~|~ {\lor} ~|~ \dots |
91 symbol & = & {\forall} ~|~ {\exists} ~|~ {\land} ~|~ {\lor} ~|~ \dots\\ |
|
92 sletter & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\ |
|
93 xletter & = & {\tt \backslash<} ~ (sletter ~|~ dletter ~|~ gletter ~|~ cletter) ~ {\tt >}\\ |
|
94 dletter & = & \verb,aa, ~|~ \dots ~|~ \verb,zz, ~|~ \verb,AA, ~|~ \dots ~|~ \verb,ZZ, \\ |
|
95 bletter & = & {\tt bool} ~|~ {\tt complex} ~|~ {\tt nat} ~|~ {\tt rat} ~|~ {\tt real} ~|~ {\tt int}\\ |
|
96 cletter & = & {\tt \hat{}\, isup} ~~|~~ {\tt \hat{}\, isub} |
|
97 \end{matharray} |
|
98 \begin{matharray}{rcl} |
|
99 gletter & = & {\tt alpha} ~|~ {\tt beta} ~|~ {\tt gamma} ~|~ {\tt delta} ~|~ {\tt epsilon} ~|~ {\tt zeta} ~|~ {\tt eta} ~|\\ |
|
100 & & {\tt theta} ~|~ {\tt iota} ~|~ {\tt kappa} ~|~ {\tt mu} ~|~ {\tt nu} ~|~ {\tt xi} ~|~ {\tt pi} ~|~ {\tt rho} ~|\\ |
|
101 & & {\tt sigma} ~|~ {\tt tau} ~|~ {\tt upsilon} ~|~ {\tt phi} ~|~ {\tt psi} ~|~ {\tt omega} ~|~ {\tt Gamma} ~|\\ |
|
102 & & {\tt Delta} ~|~ {\tt Theta} ~|~ {\tt Lambda} ~|~ {\tt Xi} ~|~ {\tt Pi} ~|~ {\tt Sigma} ~|~ {\tt Upsilon} ~|\\ |
|
103 & & {\tt Phi} ~|~ {\tt Psi} ~|~ {\tt Omega} |
93 \end{matharray} |
104 \end{matharray} |
94 |
105 |
95 The syntax of $string$ admits any characters, including newlines; ``\verb|"|'' |
106 The syntax of $string$ admits any characters, including newlines; ``\verb|"|'' |
96 (double-quote) and ``\verb|\|'' (backslash) need to be escaped by a backslash. |
107 (double-quote) and ``\verb|\|'' (backslash) need to be escaped by a backslash. |
97 Note that ML-style control characters are \emph{not} supported. The body of |
108 Note that ML-style control characters are \emph{not} supported. The body of |
115 \medskip |
126 \medskip |
116 |
127 |
117 Mathematical symbols such as ``$\forall$'' are represented in plain ASCII as |
128 Mathematical symbols such as ``$\forall$'' are represented in plain ASCII as |
118 ``\verb,\<forall>,''. Concerning Isabelle itself, any sequence of the form |
129 ``\verb,\<forall>,''. Concerning Isabelle itself, any sequence of the form |
119 \verb,\<,$ident$\verb,>, (or \verb,\\<,$ident$\verb,>,) is a legal symbol. |
130 \verb,\<,$ident$\verb,>, (or \verb,\\<,$ident$\verb,>,) is a legal symbol. |
|
131 Greek letters \verb+\<alpha>+, \verb+\<beta>+, etc (apart from |
|
132 \verb+\<lambda>+), caligraphic letters in various styles, as |
|
133 well as the special \verb+\<^isub>+ and \verb+\<^isup>+ sub/superscipt |
|
134 control characters are considered proper letters and can be used as |
|
135 part of any identifier. |
|
136 |
120 Display of appropriate glyphs is a matter of front-end tools, say the |
137 Display of appropriate glyphs is a matter of front-end tools, say the |
121 user-interface of Proof~General plus the X-Symbol package, or the {\LaTeX} |
138 user-interface of Proof~General plus the X-Symbol package, or the {\LaTeX} |
122 macro setup of document output. A list of predefined Isabelle symbols is |
139 macro setup of document output. A list of predefined Isabelle symbols is |
123 given in \cite[appendix~A]{isabelle-sys}. |
140 given in \cite[appendix~A]{isabelle-sys}. |
124 |
141 |