--- a/doc-src/System/IsaMakefile Mon Sep 15 20:51:40 2008 +0200
+++ b/doc-src/System/IsaMakefile Mon Sep 15 20:51:58 2008 +0200
@@ -21,8 +21,8 @@
Pure-System: $(LOG)/Pure-System.gz
-$(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML \
- Thy/Basics.thy Thy/Misc.thy Thy/Presentation.thy
+$(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML \
+ Thy/Basics.thy Thy/Misc.thy Thy/Presentation.thy Thy/Symbols.thy
@$(USEDIR) -s System Pure Thy
--- a/doc-src/System/Makefile Mon Sep 15 20:51:40 2008 +0200
+++ b/doc-src/System/Makefile Mon Sep 15 20:51:58 2008 +0200
@@ -12,10 +12,9 @@
include ../Makefile.in
NAME = system
-FILES = system.tex Thy/document/Basics.tex Thy/document/Misc.tex \
- Thy/document/Presentation.tex symbols.tex ../iman.sty \
- ../extra.sty ../ttbox.sty ../manual.bib \
-
+FILES = system.tex Thy/document/Basics.tex Thy/document/Misc.tex \
+ Thy/document/Presentation.tex Thy/document/Symbols.tex \
+ ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
OUTPUT = syms.tex
syms.tex: showsymbols ../isabellesym.sty
--- a/doc-src/System/Thy/ROOT.ML Mon Sep 15 20:51:40 2008 +0200
+++ b/doc-src/System/Thy/ROOT.ML Mon Sep 15 20:51:58 2008 +0200
@@ -7,3 +7,4 @@
use_thy "Basics";
use_thy "Presentation";
use_thy "Misc";
+use_thy "Symbols";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/System/Thy/Symbols.thy Mon Sep 15 20:51:58 2008 +0200
@@ -0,0 +1,49 @@
+(* $Id$ *)
+
+theory Symbols
+imports Pure
+begin
+
+chapter {* Standard Isabelle symbols \label{app:symbols} *}
+
+text {*
+ Isabelle supports an infinite number of non-ASCII symbols, which are
+ represented in source text as @{verbatim "\\"}@{verbatim "<"}@{text
+ name}@{verbatim ">"} (where @{text 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 @{verbatim "\\"}@{verbatim isasym}@{text
+ name} for each @{verbatim "\\"}@{verbatim "<"}@{text name}@{verbatim
+ ">"} in the @{verbatim 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
+ @{verbatim "\\"}@{verbatim "<^sup>"}, for superscript and @{verbatim
+ "\\"}@{verbatim "<^sub>"}, for subscript, such as @{verbatim
+ "A\\"}@{verbatim "<^sup>\<star>"}, for @{text "A\<^sup>\<star>"} the alternative
+ versions @{verbatim "\\"}@{verbatim "<^isub>"} and @{verbatim
+ "\\"}@{verbatim "<^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 @{verbatim "\\"}@{verbatim
+ "<^bsub>"}@{text "\<dots>"}@{verbatim "\\"}@{verbatim "<^esub>"}, and
+ @{verbatim "\\"}@{verbatim "<^bsup>"}@{text "\<dots>"}@{verbatim
+ "\\"}@{verbatim "<^esup>"} respectively. Furthermore, all ASCII
+ characters and most other symbols may be printed in bold by
+ prefixing @{verbatim "\\"}@{verbatim "<^bold>"} such as @{verbatim
+ "\\"}@{verbatim "<^bold>\\"}@{verbatim "<alpha>"} for @{text
+ "\<^bold>\<alpha>"}. Note that @{verbatim "\\"}@{verbatim "<^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
\ No newline at end of file
--- /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:
--- a/doc-src/System/symbols.tex Mon Sep 15 20:51:40 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-
-% $Id$
-
-\chapter{Standard Isabelle symbols}\label{app:symbols}
-
-Isabelle supports an infinite number of non-ASCII symbols, which are
-represented in source text as \verb,\<,$name$\verb,>, (where $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,\isasym,$name$ for each \verb,\<,$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,\<^sup>, for superscript and \verb,\<^sub>, for subscript, such as
-\verb,A\<^sup>\<star>, for \isa{A\isactrlsup{\isasymstar}}; the alternative
-versions \verb,\<^isub>, and \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,\<^bsub>,\dots\verb,\<^esub>, and
-\verb,\<^bsup>,\dots\verb,\<^esup>,, respectively. Furthermore, all ASCII
-characters and most other symbols may be printed in bold by prefixing
-\verb,\<^bold>,, such as \verb,\<^bold>\<alpha>, for
-\isa{\isactrlbold{\isasymalpha}}. Note that \verb,\<^bold>, may \emph{not} be
-combined with sub- or superscripts for single symbols.
-
-Further details of Isabelle document preparation are covered in
-chapter~\ref{ch:present}.
-
-\begin{center}
- \begin{isabellebody}
- \input{syms}
- \end{isabellebody}
-\end{center}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "system"
-%%% End:
--- a/doc-src/System/system.tex Mon Sep 15 20:51:40 2008 +0200
+++ b/doc-src/System/system.tex Mon Sep 15 20:51:58 2008 +0200
@@ -42,7 +42,7 @@
\appendix
\let\int\intorig
-\input{symbols}
+\input{Thy/document/Symbols}
\begingroup
\bibliographystyle{plain} \small\raggedright\frenchspacing