doc-src/IsarRef/Thy/document/Symbols.tex
author wenzelm
Fri Oct 29 11:49:56 2010 +0200 (2010-10-29)
changeset 40255 9ffbc25e1606
parent 30242 aea5d7fa7ef5
child 40406 313a24b66a8d
permissions -rw-r--r--
eliminated obsolete \_ escapes in rail environments;
wenzelm@28838
     1
%
wenzelm@28838
     2
\begin{isabellebody}%
wenzelm@28838
     3
\def\isabellecontext{Symbols}%
wenzelm@28838
     4
%
wenzelm@28838
     5
\isadelimtheory
wenzelm@28838
     6
%
wenzelm@28838
     7
\endisadelimtheory
wenzelm@28838
     8
%
wenzelm@28838
     9
\isatagtheory
wenzelm@28838
    10
\isacommand{theory}\isamarkupfalse%
wenzelm@28838
    11
\ Symbols\isanewline
wenzelm@28838
    12
\isakeyword{imports}\ Pure\isanewline
wenzelm@28838
    13
\isakeyword{begin}%
wenzelm@28838
    14
\endisatagtheory
wenzelm@28838
    15
{\isafoldtheory}%
wenzelm@28838
    16
%
wenzelm@28838
    17
\isadelimtheory
wenzelm@28838
    18
%
wenzelm@28838
    19
\endisadelimtheory
wenzelm@28838
    20
%
wenzelm@29722
    21
\isamarkupchapter{Predefined Isabelle symbols \label{app:symbols}%
wenzelm@28838
    22
}
wenzelm@28838
    23
\isamarkuptrue%
wenzelm@28838
    24
%
wenzelm@28838
    25
\begin{isamarkuptext}%
wenzelm@28838
    26
Isabelle supports an infinite number of non-ASCII symbols, which are
wenzelm@28838
    27
  represented in source text as \verb|\|\verb|<|\isa{name}\verb|>| (where \isa{name} may be any identifier).  It
wenzelm@28838
    28
  is left to front-end tools how to present these symbols to the user.
wenzelm@28838
    29
  The collection of predefined standard symbols given below is
wenzelm@28838
    30
  available by default for Isabelle document output, due to
wenzelm@28838
    31
  appropriate definitions of \verb|\|\verb|isasym|\isa{name} for each \verb|\|\verb|<|\isa{name}\verb|>| in the \verb|isabellesym.sty| file.  Most of these symbols
wenzelm@28838
    32
  are displayed properly in Proof~General if used with the X-Symbol
wenzelm@28838
    33
  package.
wenzelm@28838
    34
wenzelm@28838
    35
  Moreover, any single symbol (or ASCII character) may be prefixed by
wenzelm@28838
    36
  \verb|\|\verb|<^sup>|, for superscript and \verb|\|\verb|<^sub>|, for subscript, such as \verb|A\|\verb|<^sup>\<star>|, for \isa{{\isachardoublequote}A\isactrlsup {\isasymstar}{\isachardoublequote}} the alternative
wenzelm@28838
    37
  versions \verb|\|\verb|<^isub>| and \verb|\|\verb|<^isup>| are considered as quasi letters and may
wenzelm@28838
    38
  be used within identifiers.  Sub- and superscripts that span a
wenzelm@28838
    39
  region of text are marked up with \verb|\|\verb|<^bsub>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esub>|, and
wenzelm@28838
    40
  \verb|\|\verb|<^bsup>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esup>| respectively.  Furthermore, all ASCII
wenzelm@28838
    41
  characters and most other symbols may be printed in bold by
wenzelm@28838
    42
  prefixing \verb|\|\verb|<^bold>| such as \verb|\|\verb|<^bold>\|\verb|<alpha>| for \isa{{\isachardoublequote}\isactrlbold {\isasymalpha}{\isachardoublequote}}.  Note that \verb|\|\verb|<^bold>|, may
wenzelm@28838
    43
  \emph{not} be combined with sub- or superscripts for single symbols.
wenzelm@28838
    44
wenzelm@28838
    45
  Further details of Isabelle document preparation are covered in
wenzelm@28838
    46
  \chref{ch:document-prep}.
wenzelm@28838
    47
wenzelm@28838
    48
  \begin{center}
wenzelm@28838
    49
  \begin{isabellebody}
wenzelm@28838
    50
  \input{syms}  
wenzelm@28838
    51
  \end{isabellebody}
wenzelm@28838
    52
  \end{center}%
wenzelm@28838
    53
\end{isamarkuptext}%
wenzelm@28838
    54
\isamarkuptrue%
wenzelm@28838
    55
%
wenzelm@28838
    56
\isadelimtheory
wenzelm@28838
    57
%
wenzelm@28838
    58
\endisadelimtheory
wenzelm@28838
    59
%
wenzelm@28838
    60
\isatagtheory
wenzelm@28838
    61
\isacommand{end}\isamarkupfalse%
wenzelm@28838
    62
%
wenzelm@28838
    63
\endisatagtheory
wenzelm@28838
    64
{\isafoldtheory}%
wenzelm@28838
    65
%
wenzelm@28838
    66
\isadelimtheory
wenzelm@28838
    67
%
wenzelm@28838
    68
\endisadelimtheory
wenzelm@28838
    69
\end{isabellebody}%
wenzelm@28838
    70
%%% Local Variables:
wenzelm@28838
    71
%%% mode: latex
wenzelm@28838
    72
%%% TeX-master: "root"
wenzelm@28838
    73
%%% End: