--- a/doc-src/System/Makefile Mon Dec 04 17:30:40 2000 +0100
+++ b/doc-src/System/Makefile Mon Dec 04 23:16:25 2000 +0100
@@ -12,12 +12,15 @@
include ../Makefile.in
NAME = system
-FILES = system.tex basics.tex misc.tex fonts.tex present.tex \
+FILES = system.tex basics.tex misc.tex fonts.tex present.tex symbols.tex \
../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
+syms.tex: showsymbols ../../Distribution/lib/texinputs/isabellesym.sty
+ @./showsymbols <../../Distribution/lib/texinputs/isabellesym.sty >syms.tex
+
dvi: $(NAME).dvi
-$(NAME).dvi: $(FILES) isabelle.eps
+$(NAME).dvi: $(FILES) isabelle.eps syms.tex
$(LATEX) $(NAME)
$(BIBTEX) $(NAME)
$(LATEX) $(NAME)
@@ -27,7 +30,7 @@
pdf: $(NAME).pdf
-$(NAME).pdf: $(FILES) isabelle.pdf
+$(NAME).pdf: $(FILES) isabelle.pdf syms.tex
$(PDFLATEX) $(NAME)
$(BIBTEX) $(NAME)
$(PDFLATEX) $(NAME)
--- a/doc-src/System/present.tex Mon Dec 04 17:30:40 2000 +0100
+++ b/doc-src/System/present.tex Mon Dec 04 23:16:25 2000 +0100
@@ -1,7 +1,7 @@
%% $Id$
-\chapter{Presenting theories}
+\chapter{Presenting theories}\label{ch:present}
Isabelle provides several ways to present the outcome of formal developments,
including WWW-based browsable libraries or actual printable documents.
@@ -303,9 +303,9 @@
If the text contains any references to Isabelle symbols (such as
\verb,\<forall>,) then \texttt{isabellesym.sty} should be included as well.
This package contains a standard set of {\LaTeX} macro definitions
-\verb,\isasym,$foo$ corresponding to \verb,\<,$foo$\verb,>,. The user may
-refer to further symbols as well, simply by providing {\LaTeX} macros of the
-same sort.
+\verb,\isasym,$foo$ corresponding to \verb,\<,$foo$\verb,>, (see
+Appendix~\ref{app:symbols} for a complete list). The user may refer to
+further symbols as well, simply by providing {\LaTeX} macros of the same sort.
For proper setup of PDF documents (with hyperlinks, bookmarks, and thumbnail
images), we recommend to include \verb,pdfsetup.sty, as well. It is safe to
@@ -518,7 +518,6 @@
\S\ref{sec:tool-mkdir}) creates \texttt{IsaMakefile}s with proper invocation
of \texttt{usedir} as well.
-
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "system"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/System/symbols.tex Mon Dec 04 23:16:25 2000 +0100
@@ -0,0 +1,26 @@
+
+% $Id$
+
+\chapter{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 these symbols are presented to
+the user. The following predefined standard symbols are available by default
+for Isabelle document output; they are also supported by Proof~General when
+used together with the X-Symbol package.
+
+\begin{center}
+ \input{syms}
+\end{center}
+
+Any symbol (or plain ASCII character) may be prefixed by a control sequence
+\verb,\<^sup>, for superscript and \verb,\<^sub>, for subscript. E.g.\
+\verb,A\<^sup>\<star>, is presented in {\LaTeX} as
+\isa{A\isactrlsup{\isasymstar}}. See also Chapter~\ref{ch:present} for more
+information on Isabelle document preparation and related issues.
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "system"
+%%% End:
--- a/doc-src/System/system.tex Mon Dec 04 17:30:40 2000 +0100
+++ b/doc-src/System/system.tex Mon Dec 04 23:16:25 2000 +0100
@@ -2,8 +2,16 @@
%% $Id$
\documentclass[12pt,a4paper]{report}
-\usepackage{graphicx,../iman,../extra,../ttbox,../pdfsetup}
+\usepackage{latexsym}
+\usepackage{amssymb}
+\usepackage[english]{babel}
+\usepackage[latin1]{inputenc}
+\usepackage[only,bigsqcap]{stmaryrd}
+\usepackage{wasysym}
+\usepackage{supertabular}
+\usepackage{graphicx,../iman,../extra,../ttbox,../../Distribution/lib/texinputs/isabelle,../../Distribution/lib/texinputs/isabellesym,../pdfsetup}
+\isabellestyle{it}
\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle System Manual}
@@ -30,6 +38,9 @@
\include{misc}
\include{fonts}
+\appendix
+\include{symbols}
+
\begingroup
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{../manual}