--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/System/Thy/document/Symbols.tex Mon Sep 15 20:51:58 2008 +0200
@@ -0,0 +1,75 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Symbols}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Symbols\isanewline
+\isakeyword{imports}\ Pure\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Standard Isabelle symbols \label{app:symbols}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle supports an infinite number of non-ASCII symbols, which are
+ represented in source text as \verb|\|\verb|<|\isa{name}\verb|>| (where \isa{name} may be any identifier). It
+ is left to front-end tools how to present these symbols to the user.
+ The collection of predefined standard symbols given below is
+ available by default for Isabelle document output, due to
+ 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
+ are displayed properly in Proof~General if used with the X-Symbol
+ package.
+
+ Moreover, any single symbol (or ASCII character) may be prefixed by
+ \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
+ versions \verb|\|\verb|<^isub>| and \verb|\|\verb|<^isup>| are considered as quasi letters and may
+ be used within identifiers. Sub- and superscripts that span a
+ region of text are marked up with \verb|\|\verb|<^bsub>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esub>|, and
+ \verb|\|\verb|<^bsup>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esup>| respectively. Furthermore, all ASCII
+ characters and most other symbols may be printed in bold by
+ prefixing \verb|\|\verb|<^bold>| such as \verb|\|\verb|<^bold>\|\verb|<alpha>| for \isa{{\isachardoublequote}\isactrlbold {\isasymalpha}{\isachardoublequote}}. Note that \verb|\|\verb|<^bold>|, may
+ \emph{not} be combined with sub- or superscripts for single symbols.
+
+ Further details of Isabelle document preparation are covered in
+ \chref{ch:present}.
+
+ \begin{center}
+ \begin{isabellebody}
+ \input{syms}
+ \end{isabellebody}
+ \end{center}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: