src/Doc/Isar_Ref/Symbols.thy
author wenzelm
Wed Mar 25 11:39:52 2015 +0100 (2015-03-25)
changeset 59809 87641097d0f3
parent 58724 e5f809f52f26
child 61493 0debd22f0c0e
permissions -rw-r--r--
tuned signature;
     1 theory Symbols
     2 imports Base Main
     3 begin
     4 
     5 chapter \<open>Predefined Isabelle symbols \label{app:symbols}\<close>
     6 
     7 text \<open>
     8   Isabelle supports an infinite number of non-ASCII symbols, which are
     9   represented in source text as @{verbatim \<open>\\<close>}@{verbatim "<"}@{text
    10   name}@{verbatim ">"} (where @{text name} may be any identifier).  It
    11   is left to front-end tools how to present these symbols to the user.
    12   The collection of predefined standard symbols given below is
    13   available by default for Isabelle document output, due to
    14   appropriate definitions of @{verbatim \<open>\isasym\<close>}@{text
    15   name} for each @{verbatim \<open>\\<close>}@{verbatim "<"}@{text name}@{verbatim
    16   ">"} in the @{verbatim isabellesym.sty} file.  Most of these symbols
    17   are displayed properly in Isabelle/jEdit and {\LaTeX} generated from Isabelle.
    18 
    19   Moreover, any single symbol (or ASCII character) may be prefixed by
    20   @{verbatim "\<^sup>"} for superscript and @{verbatim "\<^sub>"} for subscript,
    21   such as @{verbatim "A\<^sup>\<star>"} for @{text "A\<^sup>\<star>"} and @{verbatim "A\<^sub>1"} for
    22   @{text "A\<^sub>1"}.  Sub- and superscripts that span a region of text can
    23   be marked up with @{verbatim "\<^bsub>"}@{text "\<dots>"}@{verbatim
    24   "\<^esub>"} and @{verbatim "\<^bsup>"}@{text "\<dots>"}@{verbatim "\<^esup>"}
    25   respectively, but note that there are limitations in the typographic
    26   rendering quality of this form.  Furthermore, all ASCII characters
    27   and most other symbols may be printed in bold by prefixing
    28   @{verbatim "\<^bold>"} such as @{verbatim "\<^bold>\<alpha>"} for @{text "\<^bold>\<alpha>"}.  Note that
    29   @{verbatim "\<^sup>"}, @{verbatim "\<^sub>"}, @{verbatim "\<^bold>"} cannot be combined.
    30 
    31   Further details of Isabelle document preparation are covered in
    32   \chref{ch:document-prep}.
    33 
    34   \begin{center}
    35   \begin{isabellebody}
    36   \input{syms}  
    37   \end{isabellebody}
    38   \end{center}
    39 \<close>
    40 
    41 end