# HG changeset patch
# User wenzelm
# Date 975968185 -3600
# Node ID 930ac2bfa6379cc65878b85e22e79fdc5bb7d0c8
# Parent  1db42f739ee72a1e68c1f84bf0f2424a0ef7cae4
include table of Isabelle standard symbols;

diff -r 1db42f739ee7 -r 930ac2bfa637 doc-src/System/Makefile
--- 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)
diff -r 1db42f739ee7 -r 930ac2bfa637 doc-src/System/present.tex
--- 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"
diff -r 1db42f739ee7 -r 930ac2bfa637 doc-src/System/symbols.tex
--- /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: 
diff -r 1db42f739ee7 -r 930ac2bfa637 doc-src/System/system.tex
--- 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}