moved table of standard Isabelle symbols to isar-ref manual;
authorwenzelm
Tue Nov 18 18:25:10 2008 +0100 (2008-11-18 ago)
changeset 28838d5db6dfcb34a
parent 28837 c6b17889237a
child 28839 32d498cf7595
moved table of standard Isabelle symbols to isar-ref manual;
doc-src/IsarRef/IsaMakefile
doc-src/IsarRef/Makefile
doc-src/IsarRef/Thy/Outer_Syntax.thy
doc-src/IsarRef/Thy/Proof.thy
doc-src/IsarRef/Thy/ROOT.ML
doc-src/IsarRef/Thy/Symbols.thy
doc-src/IsarRef/Thy/document/Outer_Syntax.tex
doc-src/IsarRef/Thy/document/Proof.tex
doc-src/IsarRef/Thy/document/Symbols.tex
doc-src/IsarRef/isar-ref.tex
doc-src/IsarRef/showsymbols
doc-src/System/IsaMakefile
doc-src/System/Makefile
doc-src/System/Thy/Presentation.thy
doc-src/System/Thy/ROOT.ML
doc-src/System/Thy/Symbols.thy
doc-src/System/Thy/document/Presentation.tex
doc-src/System/Thy/document/Symbols.tex
doc-src/System/showsymbols
doc-src/System/system.tex
doc-src/TutorialI/Datatype/document/Nested.tex
doc-src/TutorialI/Documents/Documents.thy
doc-src/TutorialI/Documents/document/Documents.tex
doc-src/TutorialI/Types/document/Numbers.tex
     1.1 --- a/doc-src/IsarRef/IsaMakefile	Tue Nov 18 18:22:49 2008 +0100
     1.2 +++ b/doc-src/IsarRef/IsaMakefile	Tue Nov 18 18:25:10 2008 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4    Thy/Inner_Syntax.thy Thy/Introduction.thy Thy/Outer_Syntax.thy	\
     1.5    Thy/Spec.thy Thy/Proof.thy Thy/Misc.thy Thy/Document_Preparation.thy	\
     1.6    Thy/Generic.thy Thy/HOL_Specific.thy Thy/Quick_Reference.thy		\
     1.7 -  Thy/ML_Tactic.thy
     1.8 +  Thy/Symbols.thy Thy/ML_Tactic.thy
     1.9  	@$(USEDIR) -s IsarRef HOL Thy
    1.10  
    1.11  
     2.1 --- a/doc-src/IsarRef/Makefile	Tue Nov 18 18:22:49 2008 +0100
     2.2 +++ b/doc-src/IsarRef/Makefile	Tue Nov 18 18:25:10 2008 +0100
     2.3 @@ -19,14 +19,20 @@
     2.4    Thy/document/Quick_Reference.tex Thy/document/Spec.tex		\
     2.5    Thy/document/ZF_Specific.tex Thy/document/Inner_Syntax.tex		\
     2.6    Thy/document/Introduction.tex Thy/document/Document_Preparation.tex	\
     2.7 -  Thy/document/Misc.tex Thy/document/Outer_Syntax.tex ../isar.sty	\
     2.8 -  ../rail.sty ../railsetup.sty ../proof.sty ../iman.sty ../extra.sty	\
     2.9 -  ../ttbox.sty ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty	\
    2.10 -  ../manual.bib
    2.11 +  Thy/document/Misc.tex Thy/document/Outer_Syntax.tex			\
    2.12 +  Thy/document/Symbols.tex ../isar.sty ../rail.sty ../railsetup.sty	\
    2.13 +  ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../isabelle.sty	\
    2.14 +  ../isabellesym.sty ../pdfsetup.sty ../manual.bib
    2.15 +
    2.16 +OUTPUT = syms.tex
    2.17 +
    2.18 +syms.tex: showsymbols ../isabellesym.sty
    2.19 +	@./showsymbols <../isabellesym.sty >syms.tex
    2.20 +
    2.21  
    2.22  dvi: $(NAME).dvi
    2.23  
    2.24 -$(NAME).dvi: $(FILES) isabelle_isar.eps
    2.25 +$(NAME).dvi: $(FILES) isabelle_isar.eps syms.tex
    2.26  	$(LATEX) $(NAME)
    2.27  	$(RAIL) $(NAME)
    2.28  	$(BIBTEX) $(NAME)
    2.29 @@ -37,7 +43,7 @@
    2.30  
    2.31  pdf: $(NAME).pdf
    2.32  
    2.33 -$(NAME).pdf: $(FILES) isabelle_isar.pdf
    2.34 +$(NAME).pdf: $(FILES) isabelle_isar.pdf syms.tex
    2.35  	$(PDFLATEX) $(NAME)
    2.36  	$(RAIL) $(NAME)
    2.37  	$(BIBTEX) $(NAME)
     3.1 --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Tue Nov 18 18:22:49 2008 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Tue Nov 18 18:25:10 2008 +0100
     3.3 @@ -171,9 +171,9 @@
     3.4    symbols like this, although proper presentation is left to front-end
     3.5    tools such as {\LaTeX} or Proof~General with the X-Symbol package.
     3.6    A list of standard Isabelle symbols that work well with these tools
     3.7 -  is given in \cite[appendix~A]{isabelle-sys}.  Note that @{verbatim
     3.8 -  "\<lambda>"} does not belong to the @{text letter} category, since it is
     3.9 -  already used differently in the Pure term language.
    3.10 +  is given in \appref{app:symbols}.  Note that @{verbatim "\<lambda>"} does
    3.11 +  not belong to the @{text letter} category, since it is already used
    3.12 +  differently in the Pure term language.
    3.13  *}
    3.14  
    3.15  
     4.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Tue Nov 18 18:22:49 2008 +0100
     4.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Tue Nov 18 18:25:10 2008 +0100
     4.3 @@ -105,7 +105,7 @@
     4.4  
     4.5    A typical application of @{command "oops"} is to explain Isar proofs
     4.6    \emph{within} the system itself, in conjunction with the document
     4.7 -  preparation tools of Isabelle described in \cite{isabelle-sys}.
     4.8 +  preparation tools of Isabelle described in \chref{ch:document-prep}.
     4.9    Thus partial or even wrong proof attempts can be discussed in a
    4.10    logically sound manner.  Note that the Isabelle {\LaTeX} macros can
    4.11    be easily adapted to print something like ``@{text "\<dots>"}'' instead of
     5.1 --- a/doc-src/IsarRef/Thy/ROOT.ML	Tue Nov 18 18:22:49 2008 +0100
     5.2 +++ b/doc-src/IsarRef/Thy/ROOT.ML	Tue Nov 18 18:25:10 2008 +0100
     5.3 @@ -14,4 +14,5 @@
     5.4  use_thy "Generic";
     5.5  use_thy "HOL_Specific";
     5.6  use_thy "Quick_Reference";
     5.7 +use_thy "Symbols";
     5.8  use_thy "ML_Tactic";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/doc-src/IsarRef/Thy/Symbols.thy	Tue Nov 18 18:25:10 2008 +0100
     6.3 @@ -0,0 +1,49 @@
     6.4 +(* $Id$ *)
     6.5 +
     6.6 +theory Symbols
     6.7 +imports Pure
     6.8 +begin
     6.9 +
    6.10 +chapter {* Standard Isabelle symbols \label{app:symbols} *}
    6.11 +
    6.12 +text {*
    6.13 +  Isabelle supports an infinite number of non-ASCII symbols, which are
    6.14 +  represented in source text as @{verbatim "\\"}@{verbatim "<"}@{text
    6.15 +  name}@{verbatim ">"} (where @{text name} may be any identifier).  It
    6.16 +  is left to front-end tools how to present these symbols to the user.
    6.17 +  The collection of predefined standard symbols given below is
    6.18 +  available by default for Isabelle document output, due to
    6.19 +  appropriate definitions of @{verbatim "\\"}@{verbatim isasym}@{text
    6.20 +  name} for each @{verbatim "\\"}@{verbatim "<"}@{text name}@{verbatim
    6.21 +  ">"} in the @{verbatim isabellesym.sty} file.  Most of these symbols
    6.22 +  are displayed properly in Proof~General if used with the X-Symbol
    6.23 +  package.
    6.24 +
    6.25 +  Moreover, any single symbol (or ASCII character) may be prefixed by
    6.26 +  @{verbatim "\\"}@{verbatim "<^sup>"}, for superscript and @{verbatim
    6.27 +  "\\"}@{verbatim "<^sub>"}, for subscript, such as @{verbatim
    6.28 +  "A\\"}@{verbatim "<^sup>\<star>"}, for @{text "A\<^sup>\<star>"} the alternative
    6.29 +  versions @{verbatim "\\"}@{verbatim "<^isub>"} and @{verbatim
    6.30 +  "\\"}@{verbatim "<^isup>"} are considered as quasi letters and may
    6.31 +  be used within identifiers.  Sub- and superscripts that span a
    6.32 +  region of text are marked up with @{verbatim "\\"}@{verbatim
    6.33 +  "<^bsub>"}@{text "\<dots>"}@{verbatim "\\"}@{verbatim "<^esub>"}, and
    6.34 +  @{verbatim "\\"}@{verbatim "<^bsup>"}@{text "\<dots>"}@{verbatim
    6.35 +  "\\"}@{verbatim "<^esup>"} respectively.  Furthermore, all ASCII
    6.36 +  characters and most other symbols may be printed in bold by
    6.37 +  prefixing @{verbatim "\\"}@{verbatim "<^bold>"} such as @{verbatim
    6.38 +  "\\"}@{verbatim "<^bold>\\"}@{verbatim "<alpha>"} for @{text
    6.39 +  "\<^bold>\<alpha>"}.  Note that @{verbatim "\\"}@{verbatim "<^bold>"}, may
    6.40 +  \emph{not} be combined with sub- or superscripts for single symbols.
    6.41 +
    6.42 +  Further details of Isabelle document preparation are covered in
    6.43 +  \chref{ch:document-prep}.
    6.44 +
    6.45 +  \begin{center}
    6.46 +  \begin{isabellebody}
    6.47 +  \input{syms}  
    6.48 +  \end{isabellebody}
    6.49 +  \end{center}
    6.50 +*}
    6.51 +
    6.52 +end
    6.53 \ No newline at end of file
     7.1 --- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Tue Nov 18 18:22:49 2008 +0100
     7.2 +++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Tue Nov 18 18:25:10 2008 +0100
     7.3 @@ -186,8 +186,9 @@
     7.4    symbols like this, although proper presentation is left to front-end
     7.5    tools such as {\LaTeX} or Proof~General with the X-Symbol package.
     7.6    A list of standard Isabelle symbols that work well with these tools
     7.7 -  is given in \cite[appendix~A]{isabelle-sys}.  Note that \verb|\<lambda>| does not belong to the \isa{letter} category, since it is
     7.8 -  already used differently in the Pure term language.%
     7.9 +  is given in \appref{app:symbols}.  Note that \verb|\<lambda>| does
    7.10 +  not belong to the \isa{letter} category, since it is already used
    7.11 +  differently in the Pure term language.%
    7.12  \end{isamarkuptext}%
    7.13  \isamarkuptrue%
    7.14  %
     8.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Tue Nov 18 18:22:49 2008 +0100
     8.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Tue Nov 18 18:25:10 2008 +0100
     8.3 @@ -128,7 +128,7 @@
     8.4  
     8.5    A typical application of \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} is to explain Isar proofs
     8.6    \emph{within} the system itself, in conjunction with the document
     8.7 -  preparation tools of Isabelle described in \cite{isabelle-sys}.
     8.8 +  preparation tools of Isabelle described in \chref{ch:document-prep}.
     8.9    Thus partial or even wrong proof attempts can be discussed in a
    8.10    logically sound manner.  Note that the Isabelle {\LaTeX} macros can
    8.11    be easily adapted to print something like ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' instead of
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/doc-src/IsarRef/Thy/document/Symbols.tex	Tue Nov 18 18:25:10 2008 +0100
     9.3 @@ -0,0 +1,75 @@
     9.4 +%
     9.5 +\begin{isabellebody}%
     9.6 +\def\isabellecontext{Symbols}%
     9.7 +%
     9.8 +\isadelimtheory
     9.9 +\isanewline
    9.10 +\isanewline
    9.11 +%
    9.12 +\endisadelimtheory
    9.13 +%
    9.14 +\isatagtheory
    9.15 +\isacommand{theory}\isamarkupfalse%
    9.16 +\ Symbols\isanewline
    9.17 +\isakeyword{imports}\ Pure\isanewline
    9.18 +\isakeyword{begin}%
    9.19 +\endisatagtheory
    9.20 +{\isafoldtheory}%
    9.21 +%
    9.22 +\isadelimtheory
    9.23 +%
    9.24 +\endisadelimtheory
    9.25 +%
    9.26 +\isamarkupchapter{Standard Isabelle symbols \label{app:symbols}%
    9.27 +}
    9.28 +\isamarkuptrue%
    9.29 +%
    9.30 +\begin{isamarkuptext}%
    9.31 +Isabelle supports an infinite number of non-ASCII symbols, which are
    9.32 +  represented in source text as \verb|\|\verb|<|\isa{name}\verb|>| (where \isa{name} may be any identifier).  It
    9.33 +  is left to front-end tools how to present these symbols to the user.
    9.34 +  The collection of predefined standard symbols given below is
    9.35 +  available by default for Isabelle document output, due to
    9.36 +  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
    9.37 +  are displayed properly in Proof~General if used with the X-Symbol
    9.38 +  package.
    9.39 +
    9.40 +  Moreover, any single symbol (or ASCII character) may be prefixed by
    9.41 +  \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
    9.42 +  versions \verb|\|\verb|<^isub>| and \verb|\|\verb|<^isup>| are considered as quasi letters and may
    9.43 +  be used within identifiers.  Sub- and superscripts that span a
    9.44 +  region of text are marked up with \verb|\|\verb|<^bsub>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esub>|, and
    9.45 +  \verb|\|\verb|<^bsup>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esup>| respectively.  Furthermore, all ASCII
    9.46 +  characters and most other symbols may be printed in bold by
    9.47 +  prefixing \verb|\|\verb|<^bold>| such as \verb|\|\verb|<^bold>\|\verb|<alpha>| for \isa{{\isachardoublequote}\isactrlbold {\isasymalpha}{\isachardoublequote}}.  Note that \verb|\|\verb|<^bold>|, may
    9.48 +  \emph{not} be combined with sub- or superscripts for single symbols.
    9.49 +
    9.50 +  Further details of Isabelle document preparation are covered in
    9.51 +  \chref{ch:document-prep}.
    9.52 +
    9.53 +  \begin{center}
    9.54 +  \begin{isabellebody}
    9.55 +  \input{syms}  
    9.56 +  \end{isabellebody}
    9.57 +  \end{center}%
    9.58 +\end{isamarkuptext}%
    9.59 +\isamarkuptrue%
    9.60 +%
    9.61 +\isadelimtheory
    9.62 +%
    9.63 +\endisadelimtheory
    9.64 +%
    9.65 +\isatagtheory
    9.66 +\isacommand{end}\isamarkupfalse%
    9.67 +%
    9.68 +\endisatagtheory
    9.69 +{\isafoldtheory}%
    9.70 +%
    9.71 +\isadelimtheory
    9.72 +%
    9.73 +\endisadelimtheory
    9.74 +\end{isabellebody}%
    9.75 +%%% Local Variables:
    9.76 +%%% mode: latex
    9.77 +%%% TeX-master: "root"
    9.78 +%%% End:
    10.1 --- a/doc-src/IsarRef/isar-ref.tex	Tue Nov 18 18:22:49 2008 +0100
    10.2 +++ b/doc-src/IsarRef/isar-ref.tex	Tue Nov 18 18:25:10 2008 +0100
    10.3 @@ -2,7 +2,14 @@
    10.4  %% $Id$
    10.5  
    10.6  \documentclass[12pt,a4paper,fleqn]{report}
    10.7 -\usepackage{latexsym,graphicx}
    10.8 +\usepackage{amssymb}
    10.9 +\usepackage[greek,english]{babel}
   10.10 +\usepackage[latin1]{inputenc}
   10.11 +\usepackage[only,bigsqcap]{stmaryrd}
   10.12 +\usepackage{textcomp}
   10.13 +\usepackage{latexsym}
   10.14 +\usepackage{graphicx}
   10.15 +\let\intorig=\int  %iman.sty redefines \int
   10.16  \usepackage{../iman,../extra,../isar,../proof}
   10.17  \usepackage[nohyphen,strings]{../underscore}
   10.18  \usepackage{../isabelle,../isabellesym}
   10.19 @@ -89,6 +96,8 @@
   10.20  
   10.21  \appendix
   10.22  \input{Thy/document/Quick_Reference.tex}
   10.23 +\let\int\intorig
   10.24 +\input{Thy/document/Symbols.tex}
   10.25  \input{Thy/document/ML_Tactic.tex}
   10.26  
   10.27  \begingroup
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/doc-src/IsarRef/showsymbols	Tue Nov 18 18:25:10 2008 +0100
    11.3 @@ -0,0 +1,28 @@
    11.4 +#!/usr/bin/env perl
    11.5 +#
    11.6 +# $Id$
    11.7 +
    11.8 +print "\\begin{supertabular}{ll\@{\\qquad}ll}\n";
    11.9 +
   11.10 +$eol = "&";
   11.11 +
   11.12 +while (<ARGV>) {
   11.13 +    if (m/^\\newcommand\{\\isasym([A-Za-z]+)\}/) {
   11.14 +       print "\\verb,\\<$1>, & {\\isasym$1} $eol\n";
   11.15 +#       print "\\verb,\\<$1>, & \\isactrlbold{\\isasym$1}~{\\isasym$1} $eol\n";
   11.16 +#       print "\\verb,\\<$1>, & B\\isactrlsup{\\isasym$1} $eol\n";
   11.17 +#       print "\\verb,\\<$1>, & B\\isactrlsub{\\isasym$1} $eol\n";
   11.18 +        if ("$eol" eq "&") {
   11.19 +            $eol = "\\\\";
   11.20 +        } else {
   11.21 +            $eol = "&";
   11.22 +        }
   11.23 +    }
   11.24 +}
   11.25 +
   11.26 +if ("$eol" eq "\\\\") {
   11.27 +    print "$eol\n";
   11.28 +}
   11.29 +
   11.30 +print "\\end{supertabular}\n";
   11.31 +
    12.1 --- a/doc-src/System/IsaMakefile	Tue Nov 18 18:22:49 2008 +0100
    12.2 +++ b/doc-src/System/IsaMakefile	Tue Nov 18 18:25:10 2008 +0100
    12.3 @@ -22,7 +22,7 @@
    12.4  Pure-System: $(LOG)/Pure-System.gz
    12.5  
    12.6  $(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML		\
    12.7 -  Thy/Basics.thy Thy/Misc.thy Thy/Presentation.thy Thy/Symbols.thy
    12.8 +  Thy/Basics.thy Thy/Misc.thy Thy/Presentation.thy
    12.9  	@$(USEDIR) -s System Pure Thy
   12.10  
   12.11  
    13.1 --- a/doc-src/System/Makefile	Tue Nov 18 18:22:49 2008 +0100
    13.2 +++ b/doc-src/System/Makefile	Tue Nov 18 18:25:10 2008 +0100
    13.3 @@ -13,16 +13,12 @@
    13.4  
    13.5  NAME = system
    13.6  FILES = system.tex Thy/document/Basics.tex Thy/document/Misc.tex	\
    13.7 -	Thy/document/Presentation.tex Thy/document/Symbols.tex		\
    13.8 -	../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
    13.9 -OUTPUT = syms.tex
   13.10 -
   13.11 -syms.tex: showsymbols ../isabellesym.sty
   13.12 -	@./showsymbols <../isabellesym.sty >syms.tex
   13.13 +	Thy/document/Presentation.tex ../iman.sty ../extra.sty		\
   13.14 +	../ttbox.sty ../manual.bib
   13.15  
   13.16  dvi: $(NAME).dvi
   13.17  
   13.18 -$(NAME).dvi: $(FILES) isabelle.eps syms.tex
   13.19 +$(NAME).dvi: $(FILES) isabelle.eps
   13.20  	$(LATEX) $(NAME)
   13.21  	$(BIBTEX) $(NAME)
   13.22  	$(LATEX) $(NAME)
   13.23 @@ -32,7 +28,7 @@
   13.24  
   13.25  pdf: $(NAME).pdf
   13.26  
   13.27 -$(NAME).pdf: $(FILES) isabelle.pdf syms.tex
   13.28 +$(NAME).pdf: $(FILES) isabelle.pdf
   13.29  	$(PDFLATEX) $(NAME)
   13.30  	$(BIBTEX) $(NAME)
   13.31  	$(PDFLATEX) $(NAME)
    14.1 --- a/doc-src/System/Thy/Presentation.thy	Tue Nov 18 18:22:49 2008 +0100
    14.2 +++ b/doc-src/System/Thy/Presentation.thy	Tue Nov 18 18:25:10 2008 +0100
    14.3 @@ -686,8 +686,8 @@
    14.4    "isabellesym.sty"} should be included as well.  This package
    14.5    contains a standard set of {\LaTeX} macro definitions @{verbatim
    14.6    "\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim
    14.7 -  "<"}@{text foo}@{verbatim ">"}, (see \appref{app:symbols} for a
    14.8 -  complete list of predefined Isabelle symbols).  Users may invent
    14.9 +  "<"}@{text foo}@{verbatim ">"}, see \cite{isabelle-implementation} for a
   14.10 +  complete list of predefined Isabelle symbols.  Users may invent
   14.11    further symbols as well, just by providing {\LaTeX} macros in a
   14.12    similar fashion as in @{"file" "~~/lib/texinputs/isabellesym.sty"} of
   14.13    the distribution.
    15.1 --- a/doc-src/System/Thy/ROOT.ML	Tue Nov 18 18:22:49 2008 +0100
    15.2 +++ b/doc-src/System/Thy/ROOT.ML	Tue Nov 18 18:25:10 2008 +0100
    15.3 @@ -7,4 +7,3 @@
    15.4  use_thy "Basics";
    15.5  use_thy "Presentation";
    15.6  use_thy "Misc";
    15.7 -use_thy "Symbols";
    16.1 --- a/doc-src/System/Thy/Symbols.thy	Tue Nov 18 18:22:49 2008 +0100
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,49 +0,0 @@
    16.4 -(* $Id$ *)
    16.5 -
    16.6 -theory Symbols
    16.7 -imports Pure
    16.8 -begin
    16.9 -
   16.10 -chapter {* Standard Isabelle symbols \label{app:symbols} *}
   16.11 -
   16.12 -text {*
   16.13 -  Isabelle supports an infinite number of non-ASCII symbols, which are
   16.14 -  represented in source text as @{verbatim "\\"}@{verbatim "<"}@{text
   16.15 -  name}@{verbatim ">"} (where @{text name} may be any identifier).  It
   16.16 -  is left to front-end tools how to present these symbols to the user.
   16.17 -  The collection of predefined standard symbols given below is
   16.18 -  available by default for Isabelle document output, due to
   16.19 -  appropriate definitions of @{verbatim "\\"}@{verbatim isasym}@{text
   16.20 -  name} for each @{verbatim "\\"}@{verbatim "<"}@{text name}@{verbatim
   16.21 -  ">"} in the @{verbatim isabellesym.sty} file.  Most of these symbols
   16.22 -  are displayed properly in Proof~General if used with the X-Symbol
   16.23 -  package.
   16.24 -
   16.25 -  Moreover, any single symbol (or ASCII character) may be prefixed by
   16.26 -  @{verbatim "\\"}@{verbatim "<^sup>"}, for superscript and @{verbatim
   16.27 -  "\\"}@{verbatim "<^sub>"}, for subscript, such as @{verbatim
   16.28 -  "A\\"}@{verbatim "<^sup>\<star>"}, for @{text "A\<^sup>\<star>"} the alternative
   16.29 -  versions @{verbatim "\\"}@{verbatim "<^isub>"} and @{verbatim
   16.30 -  "\\"}@{verbatim "<^isup>"} are considered as quasi letters and may
   16.31 -  be used within identifiers.  Sub- and superscripts that span a
   16.32 -  region of text are marked up with @{verbatim "\\"}@{verbatim
   16.33 -  "<^bsub>"}@{text "\<dots>"}@{verbatim "\\"}@{verbatim "<^esub>"}, and
   16.34 -  @{verbatim "\\"}@{verbatim "<^bsup>"}@{text "\<dots>"}@{verbatim
   16.35 -  "\\"}@{verbatim "<^esup>"} respectively.  Furthermore, all ASCII
   16.36 -  characters and most other symbols may be printed in bold by
   16.37 -  prefixing @{verbatim "\\"}@{verbatim "<^bold>"} such as @{verbatim
   16.38 -  "\\"}@{verbatim "<^bold>\\"}@{verbatim "<alpha>"} for @{text
   16.39 -  "\<^bold>\<alpha>"}.  Note that @{verbatim "\\"}@{verbatim "<^bold>"}, may
   16.40 -  \emph{not} be combined with sub- or superscripts for single symbols.
   16.41 -
   16.42 -  Further details of Isabelle document preparation are covered in
   16.43 -  \chref{ch:present}.
   16.44 -
   16.45 -  \begin{center}
   16.46 -  \begin{isabellebody}
   16.47 -  \input{syms}  
   16.48 -  \end{isabellebody}
   16.49 -  \end{center}
   16.50 -*}
   16.51 -
   16.52 -end
   16.53 \ No newline at end of file
    17.1 --- a/doc-src/System/Thy/document/Presentation.tex	Tue Nov 18 18:22:49 2008 +0100
    17.2 +++ b/doc-src/System/Thy/document/Presentation.tex	Tue Nov 18 18:25:10 2008 +0100
    17.3 @@ -694,8 +694,8 @@
    17.4  
    17.5    If the text contains any references to Isabelle symbols (such as
    17.6    \verb|\|\verb|<forall>|) then \verb|isabellesym.sty| should be included as well.  This package
    17.7 -  contains a standard set of {\LaTeX} macro definitions \verb|\isasym|\isa{foo} corresponding to \verb|\|\verb|<|\isa{foo}\verb|>|, (see \appref{app:symbols} for a
    17.8 -  complete list of predefined Isabelle symbols).  Users may invent
    17.9 +  contains a standard set of {\LaTeX} macro definitions \verb|\isasym|\isa{foo} corresponding to \verb|\|\verb|<|\isa{foo}\verb|>|, see \cite{isabelle-implementation} for a
   17.10 +  complete list of predefined Isabelle symbols.  Users may invent
   17.11    further symbols as well, just by providing {\LaTeX} macros in a
   17.12    similar fashion as in \hyperlink{file.~~/lib/texinputs/isabellesym.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabellesym{\isachardot}sty}}}} of
   17.13    the distribution.
    18.1 --- a/doc-src/System/Thy/document/Symbols.tex	Tue Nov 18 18:22:49 2008 +0100
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,75 +0,0 @@
    18.4 -%
    18.5 -\begin{isabellebody}%
    18.6 -\def\isabellecontext{Symbols}%
    18.7 -%
    18.8 -\isadelimtheory
    18.9 -\isanewline
   18.10 -\isanewline
   18.11 -%
   18.12 -\endisadelimtheory
   18.13 -%
   18.14 -\isatagtheory
   18.15 -\isacommand{theory}\isamarkupfalse%
   18.16 -\ Symbols\isanewline
   18.17 -\isakeyword{imports}\ Pure\isanewline
   18.18 -\isakeyword{begin}%
   18.19 -\endisatagtheory
   18.20 -{\isafoldtheory}%
   18.21 -%
   18.22 -\isadelimtheory
   18.23 -%
   18.24 -\endisadelimtheory
   18.25 -%
   18.26 -\isamarkupchapter{Standard Isabelle symbols \label{app:symbols}%
   18.27 -}
   18.28 -\isamarkuptrue%
   18.29 -%
   18.30 -\begin{isamarkuptext}%
   18.31 -Isabelle supports an infinite number of non-ASCII symbols, which are
   18.32 -  represented in source text as \verb|\|\verb|<|\isa{name}\verb|>| (where \isa{name} may be any identifier).  It
   18.33 -  is left to front-end tools how to present these symbols to the user.
   18.34 -  The collection of predefined standard symbols given below is
   18.35 -  available by default for Isabelle document output, due to
   18.36 -  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
   18.37 -  are displayed properly in Proof~General if used with the X-Symbol
   18.38 -  package.
   18.39 -
   18.40 -  Moreover, any single symbol (or ASCII character) may be prefixed by
   18.41 -  \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
   18.42 -  versions \verb|\|\verb|<^isub>| and \verb|\|\verb|<^isup>| are considered as quasi letters and may
   18.43 -  be used within identifiers.  Sub- and superscripts that span a
   18.44 -  region of text are marked up with \verb|\|\verb|<^bsub>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esub>|, and
   18.45 -  \verb|\|\verb|<^bsup>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esup>| respectively.  Furthermore, all ASCII
   18.46 -  characters and most other symbols may be printed in bold by
   18.47 -  prefixing \verb|\|\verb|<^bold>| such as \verb|\|\verb|<^bold>\|\verb|<alpha>| for \isa{{\isachardoublequote}\isactrlbold {\isasymalpha}{\isachardoublequote}}.  Note that \verb|\|\verb|<^bold>|, may
   18.48 -  \emph{not} be combined with sub- or superscripts for single symbols.
   18.49 -
   18.50 -  Further details of Isabelle document preparation are covered in
   18.51 -  \chref{ch:present}.
   18.52 -
   18.53 -  \begin{center}
   18.54 -  \begin{isabellebody}
   18.55 -  \input{syms}  
   18.56 -  \end{isabellebody}
   18.57 -  \end{center}%
   18.58 -\end{isamarkuptext}%
   18.59 -\isamarkuptrue%
   18.60 -%
   18.61 -\isadelimtheory
   18.62 -%
   18.63 -\endisadelimtheory
   18.64 -%
   18.65 -\isatagtheory
   18.66 -\isacommand{end}\isamarkupfalse%
   18.67 -%
   18.68 -\endisatagtheory
   18.69 -{\isafoldtheory}%
   18.70 -%
   18.71 -\isadelimtheory
   18.72 -%
   18.73 -\endisadelimtheory
   18.74 -\end{isabellebody}%
   18.75 -%%% Local Variables:
   18.76 -%%% mode: latex
   18.77 -%%% TeX-master: "root"
   18.78 -%%% End:
    19.1 --- a/doc-src/System/showsymbols	Tue Nov 18 18:22:49 2008 +0100
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,28 +0,0 @@
    19.4 -#!/usr/bin/env perl
    19.5 -#
    19.6 -# $Id$
    19.7 -
    19.8 -print "\\begin{supertabular}{ll\@{\\qquad}ll}\n";
    19.9 -
   19.10 -$eol = "&";
   19.11 -
   19.12 -while (<ARGV>) {
   19.13 -    if (m/^\\newcommand\{\\isasym([A-Za-z]+)\}/) {
   19.14 -       print "\\verb,\\<$1>, & {\\isasym$1} $eol\n";
   19.15 -#       print "\\verb,\\<$1>, & \\isactrlbold{\\isasym$1}~{\\isasym$1} $eol\n";
   19.16 -#       print "\\verb,\\<$1>, & B\\isactrlsup{\\isasym$1} $eol\n";
   19.17 -#       print "\\verb,\\<$1>, & B\\isactrlsub{\\isasym$1} $eol\n";
   19.18 -        if ("$eol" eq "&") {
   19.19 -            $eol = "\\\\";
   19.20 -        } else {
   19.21 -            $eol = "&";
   19.22 -        }
   19.23 -    }
   19.24 -}
   19.25 -
   19.26 -if ("$eol" eq "\\\\") {
   19.27 -    print "$eol\n";
   19.28 -}
   19.29 -
   19.30 -print "\\end{supertabular}\n";
   19.31 -
    20.1 --- a/doc-src/System/system.tex	Tue Nov 18 18:22:49 2008 +0100
    20.2 +++ b/doc-src/System/system.tex	Tue Nov 18 18:25:10 2008 +0100
    20.3 @@ -2,13 +2,7 @@
    20.4  %% $Id$
    20.5  
    20.6  \documentclass[12pt,a4paper]{report}
    20.7 -\usepackage{amssymb}
    20.8 -\usepackage[greek,english]{babel}
    20.9 -\usepackage[latin1]{inputenc}
   20.10 -\usepackage[only,bigsqcap]{stmaryrd}
   20.11 -\usepackage{textcomp}
   20.12  \usepackage{supertabular}
   20.13 -\let\intorig=\int  %iman.sty redefines \int
   20.14  \usepackage{graphicx}
   20.15  \usepackage{../iman,../extra,../isar,../ttbox}
   20.16  \usepackage[nohyphen,strings]{../underscore}
   20.17 @@ -36,13 +30,9 @@
   20.18  \maketitle 
   20.19  \pagenumbering{roman} \tableofcontents \clearfirst
   20.20  
   20.21 -\input{Thy/document/Basics}
   20.22 -\input{Thy/document/Presentation}
   20.23 -\input{Thy/document/Misc}
   20.24 -
   20.25 -\appendix
   20.26 -\let\int\intorig
   20.27 -\input{Thy/document/Symbols}
   20.28 +\input{Thy/document/Basics.tex}
   20.29 +\input{Thy/document/Presentation.tex}
   20.30 +\input{Thy/document/Misc.tex}
   20.31  
   20.32  \begingroup
   20.33    \bibliographystyle{plain} \small\raggedright\frenchspacing
    21.1 --- a/doc-src/TutorialI/Datatype/document/Nested.tex	Tue Nov 18 18:22:49 2008 +0100
    21.2 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Tue Nov 18 18:25:10 2008 +0100
    21.3 @@ -119,7 +119,7 @@
    21.4  its definition is found in theorem \isa{o{\isacharunderscore}def}).
    21.5  \end{exercise}
    21.6  \begin{exercise}\label{ex:trev-trev}
    21.7 -  Define a function \isa{trev} of type \isa{{\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ term}
    21.8 +  Define a function \isa{trev} of type \isa{{\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ Nested{\isachardot}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ Nested{\isachardot}term}
    21.9  that recursively reverses the order of arguments of all function symbols in a
   21.10    term. Prove that \isa{trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t}.
   21.11  \end{exercise}
    22.1 --- a/doc-src/TutorialI/Documents/Documents.thy	Tue Nov 18 18:22:49 2008 +0100
    22.2 +++ b/doc-src/TutorialI/Documents/Documents.thy	Tue Nov 18 18:25:10 2008 +0100
    22.3 @@ -107,7 +107,7 @@
    22.4    \verb,\,\verb,<forall>, symbol as~@{text \<forall>}.
    22.5  
    22.6    A list of standard Isabelle symbols is given in
    22.7 -  \cite[appendix~A]{isabelle-sys}.  You may introduce your own
    22.8 +  \cite{isabelle-isar-ref}.  You may introduce your own
    22.9    interpretation of further symbols by configuring the appropriate
   22.10    front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
   22.11    macros (see also \S\ref{sec:doc-prep-symbols}).  There are also a
   22.12 @@ -666,7 +666,7 @@
   22.13    straightforward generalization of ASCII characters.  While Isabelle
   22.14    does not impose any interpretation of the infinite collection of
   22.15    named symbols, {\LaTeX} documents use canonical glyphs for certain
   22.16 -  standard symbols \cite[appendix~A]{isabelle-sys}.
   22.17 +  standard symbols \cite{isabelle-isar-ref}.
   22.18  
   22.19    The {\LaTeX} code produced from Isabelle text follows a simple
   22.20    scheme.  You can tune the final appearance by redefining certain
    23.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex	Tue Nov 18 18:22:49 2008 +0100
    23.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex	Tue Nov 18 18:25:10 2008 +0100
    23.3 @@ -123,7 +123,7 @@
    23.4    \verb,\,\verb,<forall>, symbol as~\isa{{\isasymforall}}.
    23.5  
    23.6    A list of standard Isabelle symbols is given in
    23.7 -  \cite[appendix~A]{isabelle-sys}.  You may introduce your own
    23.8 +  \cite{isabelle-isar-ref}.  You may introduce your own
    23.9    interpretation of further symbols by configuring the appropriate
   23.10    front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
   23.11    macros (see also \S\ref{sec:doc-prep-symbols}).  There are also a
   23.12 @@ -394,18 +394,18 @@
   23.13    (usually rooted at \verb,~/isabelle/browser_info,).
   23.14  
   23.15    \medskip The easiest way to manage Isabelle sessions is via
   23.16 -  \texttt{isatool mkdir} (generates an initial session source setup)
   23.17 -  and \texttt{isatool make} (run sessions controlled by
   23.18 +  \texttt{isabelle mkdir} (generates an initial session source setup)
   23.19 +  and \texttt{isabelle make} (run sessions controlled by
   23.20    \texttt{IsaMakefile}).  For example, a new session
   23.21    \texttt{MySession} derived from \texttt{HOL} may be produced as
   23.22    follows:
   23.23  
   23.24  \begin{verbatim}
   23.25 -  isatool mkdir HOL MySession
   23.26 -  isatool make
   23.27 +  isabelle mkdir HOL MySession
   23.28 +  isabelle make
   23.29  \end{verbatim}
   23.30  
   23.31 -  The \texttt{isatool make} job also informs about the file-system
   23.32 +  The \texttt{isabelle make} job also informs about the file-system
   23.33    location of the ultimate results.  The above dry run should be able
   23.34    to produce some \texttt{document.pdf} (with dummy title, empty table
   23.35    of contents etc.).  Any failure at this stage usually indicates
   23.36 @@ -441,7 +441,7 @@
   23.37    several sessions may be managed by the same \texttt{IsaMakefile}.
   23.38    See the \emph{Isabelle System Manual} \cite{isabelle-sys} 
   23.39    for further details, especially on
   23.40 -  \texttt{isatool usedir} and \texttt{isatool make}.
   23.41 +  \texttt{isabelle usedir} and \texttt{isabelle make}.
   23.42  
   23.43    \end{itemize}
   23.44  
   23.45 @@ -464,7 +464,7 @@
   23.46    \texttt{MySession/document} directory as well.  In particular,
   23.47    adding a file named \texttt{root.bib} causes an automatic run of
   23.48    \texttt{bibtex} to process a bibliographic database; see also
   23.49 -  \texttt{isatool document} \cite{isabelle-sys}.
   23.50 +  \texttt{isabelle document} \cite{isabelle-sys}.
   23.51  
   23.52    \medskip Any failure of the document preparation phase in an
   23.53    Isabelle batch session leaves the generated sources in their target
   23.54 @@ -741,7 +741,7 @@
   23.55    straightforward generalization of ASCII characters.  While Isabelle
   23.56    does not impose any interpretation of the infinite collection of
   23.57    named symbols, {\LaTeX} documents use canonical glyphs for certain
   23.58 -  standard symbols \cite[appendix~A]{isabelle-sys}.
   23.59 +  standard symbols \cite{isabelle-isar-ref}.
   23.60  
   23.61    The {\LaTeX} code produced from Isabelle text follows a simple
   23.62    scheme.  You can tune the final appearance by redefining certain
   23.63 @@ -844,7 +844,7 @@
   23.64    tagged region, in order to keep, drop, or fold the corresponding
   23.65    parts of the document.  See the \emph{Isabelle System Manual}
   23.66    \cite{isabelle-sys} for further details, especially on
   23.67 -  \texttt{isatool usedir} and \texttt{isatool document}.
   23.68 +  \texttt{isabelle usedir} and \texttt{isabelle document}.
   23.69  
   23.70    Ignored material is specified by delimiting the original formal
   23.71    source with special source comments
    24.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex	Tue Nov 18 18:22:49 2008 +0100
    24.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex	Tue Nov 18 18:25:10 2008 +0100
    24.3 @@ -569,9 +569,7 @@
    24.4  effect of show sorts on the above
    24.5  
    24.6  \begin{isabelle}%
    24.7 -{\isacharparenleft}{\isacharparenleft}c{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isacharequal}\isanewline
    24.8 -\isaindent{{\isacharparenleft}}c\ {\isacharasterisk}\ {\isacharparenleft}b{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
    24.9 -{\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
   24.10 +{\isacharparenleft}c\ {\isacharasterisk}\ a\ {\isacharequal}\ c\ {\isacharasterisk}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
   24.11  \end{isabelle}
   24.12  \rulename{mult_cancel_left}%
   24.13  \end{isamarkuptext}%