118 ``\verb,\<forall>,''. Concerning Isabelle itself, any sequence of the form |
118 ``\verb,\<forall>,''. Concerning Isabelle itself, any sequence of the form |
119 \verb,\<,$ident$\verb,>, (or \verb,\\<,$ident$\verb,>,) is a legal symbol. |
119 \verb,\<,$ident$\verb,>, (or \verb,\\<,$ident$\verb,>,) is a legal symbol. |
120 Display of appropriate glyphs is a matter of front-end tools, say the |
120 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} |
121 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 |
122 macro setup of document output. A list of predefined Isabelle symbols is |
123 given in \cite[Appendix~A]{isabelle-sys}. |
123 given in \cite[appendix~A]{isabelle-sys}. |
124 |
124 |
125 |
125 |
126 \section{Common syntax entities} |
126 \section{Common syntax entities} |
127 |
127 |
128 Subsequently, we introduce several basic syntactic entities, such as names, |
128 Subsequently, we introduce several basic syntactic entities, such as names, |