src/Doc/Isar_Ref/Symbols.thy
 author wenzelm Mon Oct 09 21:12:22 2017 +0200 (23 months ago) changeset 66822 4642cf4a7ebb parent 63531 847eefdca90d child 67399 eab6ce8368fa permissions -rw-r--r--
tuned signature;
     1 (*:maxLineLen=78:*)

     2

     3 theory Symbols

     4   imports Main Base

     5 begin

     6

     7 chapter \<open>Predefined Isabelle symbols \label{app:symbols}\<close>

     8

     9 text \<open>

    10   Isabelle supports an infinite number of non-ASCII symbols, which are

    11   represented in source text as \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> (where \<open>name\<close> may be any identifier).  It

    12   is left to front-end tools how to present these symbols to the user.

    13   The collection of predefined standard symbols given below is

    14   available by default for Isabelle document output, due to

    15   appropriate definitions of \<^verbatim>\<open>\isasym\<close>\<open>name\<close> for each \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> in

    16   the \<^verbatim>\<open>isabellesym.sty\<close> 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>\<open>\<^sup>\<close> for superscript and \<^verbatim>\<open>\<^sub>\<close> for subscript,

    21   such as \<^verbatim>\<open>A\<^sup>\<star>\<close> for \<open>A\<^sup>\<star>\<close> and \<^verbatim>\<open>A\<^sub>1\<close> for

    22   \<open>A\<^sub>1\<close>.  Sub- and superscripts that span a region of text can

    23   be marked up with \<^verbatim>\<open>\<^bsub>\<close>\<open>\<dots>\<close>\<^verbatim>\<open>\<^esub>\<close> and \<^verbatim>\<open>\<^bsup>\<close>\<open>\<dots>\<close>\<^verbatim>\<open>\<^esup>\<close>

    24   respectively, but note that there are limitations in the typographic

    25   rendering quality of this form.  Furthermore, all ASCII characters

    26   and most other symbols may be printed in bold by prefixing

    27   \<^verbatim>\<open>\<^bold>\<close> such as \<^verbatim>\<open>\<^bold>\<alpha>\<close> for \<open>\<^bold>\<alpha>\<close>.  Note that

    28   \<^verbatim>\<open>\<^sup>\<close>, \<^verbatim>\<open>\<^sub>\<close>, \<^verbatim>\<open>\<^bold>\<close> cannot be combined.

    29

    30   Further details of Isabelle document preparation are covered in

    31   \chref{ch:document-prep}.

    32

    33   \begin{center}

    34   \begin{isabellebody}

    35   \input{syms}

    36   \end{isabellebody}

    37   \end{center}

    38 \<close>

    39

    40 end