doc-src/IsarRef/syntax.tex
changeset 12637 4d43b06a81e1
parent 12618 43a97a2155d0
child 12879 8e1cae1de136
equal deleted inserted replaced
12636:5069929098ab 12637:4d43b06a81e1
   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,