include table of Isabelle standard symbols;
authorwenzelm
Mon Dec 04 23:16:25 2000 +0100 (2000-12-04)
changeset 10580930ac2bfa637
parent 10579 1db42f739ee7
child 10581 74e542a299f0
include table of Isabelle standard symbols;
doc-src/System/Makefile
doc-src/System/present.tex
doc-src/System/symbols.tex
doc-src/System/system.tex
     1.1 --- a/doc-src/System/Makefile	Mon Dec 04 17:30:40 2000 +0100
     1.2 +++ b/doc-src/System/Makefile	Mon Dec 04 23:16:25 2000 +0100
     1.3 @@ -12,12 +12,15 @@
     1.4  include ../Makefile.in
     1.5  
     1.6  NAME = system
     1.7 -FILES = system.tex basics.tex misc.tex fonts.tex present.tex \
     1.8 +FILES = system.tex basics.tex misc.tex fonts.tex present.tex symbols.tex \
     1.9  	../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
    1.10  
    1.11 +syms.tex: showsymbols ../../Distribution/lib/texinputs/isabellesym.sty
    1.12 +	@./showsymbols <../../Distribution/lib/texinputs/isabellesym.sty >syms.tex
    1.13 +
    1.14  dvi: $(NAME).dvi
    1.15  
    1.16 -$(NAME).dvi: $(FILES) isabelle.eps
    1.17 +$(NAME).dvi: $(FILES) isabelle.eps syms.tex
    1.18  	$(LATEX) $(NAME)
    1.19  	$(BIBTEX) $(NAME)
    1.20  	$(LATEX) $(NAME)
    1.21 @@ -27,7 +30,7 @@
    1.22  
    1.23  pdf: $(NAME).pdf
    1.24  
    1.25 -$(NAME).pdf: $(FILES) isabelle.pdf
    1.26 +$(NAME).pdf: $(FILES) isabelle.pdf syms.tex
    1.27  	$(PDFLATEX) $(NAME)
    1.28  	$(BIBTEX) $(NAME)
    1.29  	$(PDFLATEX) $(NAME)
     2.1 --- a/doc-src/System/present.tex	Mon Dec 04 17:30:40 2000 +0100
     2.2 +++ b/doc-src/System/present.tex	Mon Dec 04 23:16:25 2000 +0100
     2.3 @@ -1,7 +1,7 @@
     2.4  
     2.5  %% $Id$
     2.6  
     2.7 -\chapter{Presenting theories}
     2.8 +\chapter{Presenting theories}\label{ch:present}
     2.9  
    2.10  Isabelle provides several ways to present the outcome of formal developments,
    2.11  including WWW-based browsable libraries or actual printable documents.
    2.12 @@ -303,9 +303,9 @@
    2.13  If the text contains any references to Isabelle symbols (such as
    2.14  \verb,\<forall>,) then \texttt{isabellesym.sty} should be included as well.
    2.15  This package contains a standard set of {\LaTeX} macro definitions
    2.16 -\verb,\isasym,$foo$ corresponding to \verb,\<,$foo$\verb,>,.  The user may
    2.17 -refer to further symbols as well, simply by providing {\LaTeX} macros of the
    2.18 -same sort.
    2.19 +\verb,\isasym,$foo$ corresponding to \verb,\<,$foo$\verb,>, (see
    2.20 +Appendix~\ref{app:symbols} for a complete list).  The user may refer to
    2.21 +further symbols as well, simply by providing {\LaTeX} macros of the same sort.
    2.22  
    2.23  For proper setup of PDF documents (with hyperlinks, bookmarks, and thumbnail
    2.24  images), we recommend to include \verb,pdfsetup.sty, as well.  It is safe to
    2.25 @@ -518,7 +518,6 @@
    2.26  \S\ref{sec:tool-mkdir}) creates \texttt{IsaMakefile}s with proper invocation
    2.27  of \texttt{usedir} as well.
    2.28  
    2.29 -
    2.30  %%% Local Variables: 
    2.31  %%% mode: latex
    2.32  %%% TeX-master: "system"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/System/symbols.tex	Mon Dec 04 23:16:25 2000 +0100
     3.3 @@ -0,0 +1,26 @@
     3.4 +
     3.5 +% $Id$
     3.6 +
     3.7 +\chapter{Isabelle symbols}\label{app:symbols}
     3.8 +
     3.9 +Isabelle supports an infinite number of non-ASCII symbols, which are
    3.10 +represented in source text as \verb,\<,$name$\verb,>, (where $name$ may be any
    3.11 +identifier).  It is left to front-end tools how these symbols are presented to
    3.12 +the user.  The following predefined standard symbols are available by default
    3.13 +for Isabelle document output; they are also supported by Proof~General when
    3.14 +used together with the X-Symbol package.
    3.15 +
    3.16 +\begin{center}
    3.17 +  \input{syms}  
    3.18 +\end{center}
    3.19 +
    3.20 +Any symbol (or plain ASCII character) may be prefixed by a control sequence
    3.21 +\verb,\<^sup>, for superscript and \verb,\<^sub>, for subscript.  E.g.\ 
    3.22 +\verb,A\<^sup>\<star>, is presented in {\LaTeX} as
    3.23 +\isa{A\isactrlsup{\isasymstar}}.  See also Chapter~\ref{ch:present} for more
    3.24 +information on Isabelle document preparation and related issues.
    3.25 +
    3.26 +%%% Local Variables: 
    3.27 +%%% mode: latex
    3.28 +%%% TeX-master: "system"
    3.29 +%%% End: 
     4.1 --- a/doc-src/System/system.tex	Mon Dec 04 17:30:40 2000 +0100
     4.2 +++ b/doc-src/System/system.tex	Mon Dec 04 23:16:25 2000 +0100
     4.3 @@ -2,8 +2,16 @@
     4.4  %% $Id$
     4.5  
     4.6  \documentclass[12pt,a4paper]{report}
     4.7 -\usepackage{graphicx,../iman,../extra,../ttbox,../pdfsetup}
     4.8 +\usepackage{latexsym}
     4.9 +\usepackage{amssymb}
    4.10 +\usepackage[english]{babel}
    4.11 +\usepackage[latin1]{inputenc}
    4.12 +\usepackage[only,bigsqcap]{stmaryrd}
    4.13 +\usepackage{wasysym}
    4.14 +\usepackage{supertabular}
    4.15 +\usepackage{graphicx,../iman,../extra,../ttbox,../../Distribution/lib/texinputs/isabelle,../../Distribution/lib/texinputs/isabellesym,../pdfsetup}
    4.16  
    4.17 +\isabellestyle{it}
    4.18  
    4.19  \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle System Manual}
    4.20  
    4.21 @@ -30,6 +38,9 @@
    4.22  \include{misc}
    4.23  \include{fonts}
    4.24  
    4.25 +\appendix
    4.26 +\include{symbols}
    4.27 +
    4.28  \begingroup
    4.29    \bibliographystyle{plain} \small\raggedright\frenchspacing
    4.30    \bibliography{../manual}