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}%