# 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,\,) 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>\, 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}