wenzelm@28838: theory Symbols
wenzelm@28838: imports Pure
wenzelm@28838: begin
wenzelm@28838: 
wenzelm@30045: chapter {* Predefined Isabelle symbols \label{app:symbols} *}
wenzelm@28838: 
wenzelm@28838: text {*
wenzelm@28838:   Isabelle supports an infinite number of non-ASCII symbols, which are
wenzelm@28838:   represented in source text as @{verbatim "\\"}@{verbatim "<"}@{text
wenzelm@28838:   name}@{verbatim ">"} (where @{text name} may be any identifier).  It
wenzelm@28838:   is left to front-end tools how to present these symbols to the user.
wenzelm@28838:   The collection of predefined standard symbols given below is
wenzelm@28838:   available by default for Isabelle document output, due to
wenzelm@28838:   appropriate definitions of @{verbatim "\\"}@{verbatim isasym}@{text
wenzelm@28838:   name} for each @{verbatim "\\"}@{verbatim "<"}@{text name}@{verbatim
wenzelm@28838:   ">"} in the @{verbatim isabellesym.sty} file.  Most of these symbols
wenzelm@28838:   are displayed properly in Proof~General if used with the X-Symbol
wenzelm@28838:   package.
wenzelm@28838: 
wenzelm@28838:   Moreover, any single symbol (or ASCII character) may be prefixed by
wenzelm@28838:   @{verbatim "\\"}@{verbatim "<^sup>"}, for superscript and @{verbatim
wenzelm@28838:   "\\"}@{verbatim "<^sub>"}, for subscript, such as @{verbatim
wenzelm@28838:   "A\\"}@{verbatim "<^sup>\<star>"}, for @{text "A\<^sup>\<star>"} the alternative
wenzelm@28838:   versions @{verbatim "\\"}@{verbatim "<^isub>"} and @{verbatim
wenzelm@28838:   "\\"}@{verbatim "<^isup>"} are considered as quasi letters and may
wenzelm@28838:   be used within identifiers.  Sub- and superscripts that span a
wenzelm@28838:   region of text are marked up with @{verbatim "\\"}@{verbatim
wenzelm@28838:   "<^bsub>"}@{text "\<dots>"}@{verbatim "\\"}@{verbatim "<^esub>"}, and
wenzelm@28838:   @{verbatim "\\"}@{verbatim "<^bsup>"}@{text "\<dots>"}@{verbatim
wenzelm@28838:   "\\"}@{verbatim "<^esup>"} respectively.  Furthermore, all ASCII
wenzelm@28838:   characters and most other symbols may be printed in bold by
wenzelm@28838:   prefixing @{verbatim "\\"}@{verbatim "<^bold>"} such as @{verbatim
wenzelm@28838:   "\\"}@{verbatim "<^bold>\\"}@{verbatim "<alpha>"} for @{text
wenzelm@28838:   "\<^bold>\<alpha>"}.  Note that @{verbatim "\\"}@{verbatim "<^bold>"}, may
wenzelm@28838:   \emph{not} be combined with sub- or superscripts for single symbols.
wenzelm@28838: 
wenzelm@28838:   Further details of Isabelle document preparation are covered in
wenzelm@28838:   \chref{ch:document-prep}.
wenzelm@28838: 
wenzelm@28838:   \begin{center}
wenzelm@28838:   \begin{isabellebody}
wenzelm@28838:   \input{syms}  
wenzelm@28838:   \end{isabellebody}
wenzelm@28838:   \end{center}
wenzelm@28838: *}
wenzelm@28838: 
wenzelm@28838: end