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