--- a/doc-src/IsarRef/Thy/document/Symbols.tex Tue Aug 28 12:31:53 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Symbols}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Symbols\isanewline
-\isakeyword{imports}\ Base\ Main\isanewline
-\isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupchapter{Predefined 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 and Isabelle/jEdit.
-
- 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{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{5C3C737461723E}{\isasymstar}}{\isaliteral{22}{\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{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}\verb|\|\verb|<^esub>|, and
- \verb|\|\verb|<^bsup>|\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\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{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\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:document-prep}.
-
- \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: