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;
wenzelm@61656
     1
(*:maxLineLen=78:*)
wenzelm@61656
     2
wenzelm@28838
     3
theory Symbols
wenzelm@63531
     4
  imports Main Base
wenzelm@28838
     5
begin
wenzelm@28838
     6
wenzelm@58618
     7
chapter \<open>Predefined Isabelle symbols \label{app:symbols}\<close>
wenzelm@28838
     8
wenzelm@58618
     9
text \<open>
wenzelm@28838
    10
  Isabelle supports an infinite number of non-ASCII symbols, which are
wenzelm@61503
    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
wenzelm@28838
    12
  is left to front-end tools how to present these symbols to the user.
wenzelm@28838
    13
  The collection of predefined standard symbols given below is
wenzelm@28838
    14
  available by default for Isabelle document output, due to
wenzelm@61503
    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
wenzelm@61503
    16
  the \<^verbatim>\<open>isabellesym.sty\<close> file.  Most of these symbols
wenzelm@53060
    17
  are displayed properly in Isabelle/jEdit and {\LaTeX} generated from Isabelle.
wenzelm@28838
    18
wenzelm@28838
    19
  Moreover, any single symbol (or ASCII character) may be prefixed by
wenzelm@61503
    20
  \<^verbatim>\<open>\<^sup>\<close> for superscript and \<^verbatim>\<open>\<^sub>\<close> for subscript,
wenzelm@61503
    21
  such as \<^verbatim>\<open>A\<^sup>\<star>\<close> for \<open>A\<^sup>\<star>\<close> and \<^verbatim>\<open>A\<^sub>1\<close> for
wenzelm@61493
    22
  \<open>A\<^sub>1\<close>.  Sub- and superscripts that span a region of text can
wenzelm@61503
    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>
wenzelm@53060
    24
  respectively, but note that there are limitations in the typographic
wenzelm@53060
    25
  rendering quality of this form.  Furthermore, all ASCII characters
wenzelm@53060
    26
  and most other symbols may be printed in bold by prefixing
wenzelm@61503
    27
  \<^verbatim>\<open>\<^bold>\<close> such as \<^verbatim>\<open>\<^bold>\<alpha>\<close> for \<open>\<^bold>\<alpha>\<close>.  Note that
wenzelm@61503
    28
  \<^verbatim>\<open>\<^sup>\<close>, \<^verbatim>\<open>\<^sub>\<close>, \<^verbatim>\<open>\<^bold>\<close> cannot be combined.
wenzelm@28838
    29
wenzelm@28838
    30
  Further details of Isabelle document preparation are covered in
wenzelm@28838
    31
  \chref{ch:document-prep}.
wenzelm@28838
    32
wenzelm@28838
    33
  \begin{center}
wenzelm@28838
    34
  \begin{isabellebody}
wenzelm@28838
    35
  \input{syms}  
wenzelm@28838
    36
  \end{isabellebody}
wenzelm@28838
    37
  \end{center}
wenzelm@58618
    38
\<close>
wenzelm@28838
    39
wenzelm@28838
    40
end