doc-src/IsarRef/syntax.tex
changeset 14212 cd05b503ca2d
parent 13827 c690cb885db4
child 14483 6eac487f9cfa
equal deleted inserted replaced
14211:7286c187596d 14212:cd05b503ca2d
    73 \begin{matharray}{rcl}
    73 \begin{matharray}{rcl}
    74   ident & = & letter~quasiletter^* \\
    74   ident & = & letter~quasiletter^* \\
    75   longident & = & ident\verb,.,ident~\dots~ident \\
    75   longident & = & ident\verb,.,ident~\dots~ident \\
    76   symident & = & sym^+ ~|~ symbol \\
    76   symident & = & sym^+ ~|~ symbol \\
    77   nat & = & digit^+ \\
    77   nat & = & digit^+ \\
    78   var & = & \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 & = & \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,*}, \\
    83 \end{matharray}
    83 \end{matharray}
    84 \begin{matharray}{rcl}
    84 \begin{matharray}{rcl}
    85   letter & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
    85   letter & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\