doc-src/IsarRef/syntax.tex
changeset 20120 4fcabd21e2aa
parent 19586 a14871b57387
child 21343 320e136db6dc
equal deleted inserted replaced
20119:7923aacc10c6 20120:4fcabd21e2aa
    87          &   & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
    87          &   & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
    88   quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
    88   quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
    89   latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
    89   latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
    90   digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
    90   digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
    91   sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~  %$
    91   sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~  %$
    92    \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~ \\
    92    \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \\
    93   & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~
    93   & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~
    94   \verb,^, ~|~ \verb,_, ~|~ \verb,|, ~|~ \verb,~, \\
    94   \verb,^, ~|~ \verb,_, ~|~ \verb,|, ~|~ \verb,~, \\
    95 greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\
    95 greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\
    96       &   & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\
    96       &   & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\
    97       &   & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\
    97       &   & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\