wneuper/isa: doc-src/IsarRef/Thy/document/Symbols.tex@aea5d7fa7ef5

1 %

     2 \begin{isabellebody}%

     3 \def\isabellecontext{Symbols}%

4 %

     5 \isadelimtheory

6 %

     7 \endisadelimtheory

8 %

     9 \isatagtheory

    10 \isacommand{theory}\isamarkupfalse%

    11 \ Symbols\isanewline

    12 \isakeyword{imports}\ Pure\isanewline

    13 \isakeyword{begin}%

    14 \endisatagtheory

    15 {\isafoldtheory}%

    16 %

    17 \isadelimtheory

    18 %

    19 \endisadelimtheory

    20 %

    21 \isamarkupchapter{Predefined Isabelle symbols \label{app:symbols}%

    22 }

    23 \isamarkuptrue%

    24 %

    25 \begin{isamarkuptext}%

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

    27   represented in source text as \verb|\|\verb|<|\isa{name}\verb|>| (where \isa{name} may be any identifier).  It

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

    29   The collection of predefined standard symbols given below is

    30   available by default for Isabelle document output, due to

    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

    32   are displayed properly in Proof~General if used with the X-Symbol

    33   package.

    35   Moreover, any single symbol (or ASCII character) may be prefixed by

    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

    37   versions \verb|\|\verb|<^isub>| and \verb|\|\verb|<^isup>| are considered as quasi letters and may

    38   be used within identifiers.  Sub- and superscripts that span a

    39   region of text are marked up with \verb|\|\verb|<^bsub>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esub>|, and

    40   \verb|\|\verb|<^bsup>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esup>| respectively.  Furthermore, all ASCII

    41   characters and most other symbols may be printed in bold by

    42   prefixing \verb|\|\verb|<^bold>| such as \verb|\|\verb|<^bold>\|\verb|<alpha>| for \isa{{\isachardoublequote}\isactrlbold {\isasymalpha}{\isachardoublequote}}.  Note that \verb|\|\verb|<^bold>|, may

    43   \emph{not} be combined with sub- or superscripts for single symbols.

    45   Further details of Isabelle document preparation are covered in

    46   \chref{ch:document-prep}.

    48   \begin{center}

    49   \begin{isabellebody}

    50   \input{syms}

    51   \end{isabellebody}

    52   \end{center}%

    53 \end{isamarkuptext}%

    54 \isamarkuptrue%

    55 %

    56 \isadelimtheory

    57 %

    58 \endisadelimtheory

    59 %

    60 \isatagtheory

    61 \isacommand{end}\isamarkupfalse%

    62 %

    63 \endisatagtheory

    64 {\isafoldtheory}%

    65 %

    66 \isadelimtheory

    67 %

    68 \endisadelimtheory

    69 \end{isabellebody}%

    70 %%% Local Variables:

    71 %%% mode: latex

    72 %%% TeX-master: "root"

    73 %%% End:

author	blanchet
	Wed, 04 Mar 2009 11:05:29 +0100
changeset 30242	aea5d7fa7ef5
parent 30240	5b25fee0362c
parent 30172	afdf7808cfd0
child 40685	313a24b66a8d
permissions	-rw-r--r--