--- a/doc-src/IsarRef/IsaMakefile Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/IsarRef/IsaMakefile Tue Nov 18 18:25:10 2008 +0100
@@ -25,7 +25,7 @@
Thy/Inner_Syntax.thy Thy/Introduction.thy Thy/Outer_Syntax.thy \
Thy/Spec.thy Thy/Proof.thy Thy/Misc.thy Thy/Document_Preparation.thy \
Thy/Generic.thy Thy/HOL_Specific.thy Thy/Quick_Reference.thy \
- Thy/ML_Tactic.thy
+ Thy/Symbols.thy Thy/ML_Tactic.thy
@$(USEDIR) -s IsarRef HOL Thy
--- a/doc-src/IsarRef/Makefile Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/IsarRef/Makefile Tue Nov 18 18:25:10 2008 +0100
@@ -19,14 +19,20 @@
Thy/document/Quick_Reference.tex Thy/document/Spec.tex \
Thy/document/ZF_Specific.tex Thy/document/Inner_Syntax.tex \
Thy/document/Introduction.tex Thy/document/Document_Preparation.tex \
- Thy/document/Misc.tex Thy/document/Outer_Syntax.tex ../isar.sty \
- ../rail.sty ../railsetup.sty ../proof.sty ../iman.sty ../extra.sty \
- ../ttbox.sty ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty \
- ../manual.bib
+ Thy/document/Misc.tex Thy/document/Outer_Syntax.tex \
+ Thy/document/Symbols.tex ../isar.sty ../rail.sty ../railsetup.sty \
+ ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../isabelle.sty \
+ ../isabellesym.sty ../pdfsetup.sty ../manual.bib
+
+OUTPUT = syms.tex
+
+syms.tex: showsymbols ../isabellesym.sty
+ @./showsymbols <../isabellesym.sty >syms.tex
+
dvi: $(NAME).dvi
-$(NAME).dvi: $(FILES) isabelle_isar.eps
+$(NAME).dvi: $(FILES) isabelle_isar.eps syms.tex
$(LATEX) $(NAME)
$(RAIL) $(NAME)
$(BIBTEX) $(NAME)
@@ -37,7 +43,7 @@
pdf: $(NAME).pdf
-$(NAME).pdf: $(FILES) isabelle_isar.pdf
+$(NAME).pdf: $(FILES) isabelle_isar.pdf syms.tex
$(PDFLATEX) $(NAME)
$(RAIL) $(NAME)
$(BIBTEX) $(NAME)
--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy Tue Nov 18 18:25:10 2008 +0100
@@ -171,9 +171,9 @@
symbols like this, although proper presentation is left to front-end
tools such as {\LaTeX} or Proof~General with the X-Symbol package.
A list of standard Isabelle symbols that work well with these tools
- is given in \cite[appendix~A]{isabelle-sys}. Note that @{verbatim
- "\<lambda>"} does not belong to the @{text letter} category, since it is
- already used differently in the Pure term language.
+ is given in \appref{app:symbols}. Note that @{verbatim "\<lambda>"} does
+ not belong to the @{text letter} category, since it is already used
+ differently in the Pure term language.
*}
--- a/doc-src/IsarRef/Thy/Proof.thy Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/IsarRef/Thy/Proof.thy Tue Nov 18 18:25:10 2008 +0100
@@ -105,7 +105,7 @@
A typical application of @{command "oops"} is to explain Isar proofs
\emph{within} the system itself, in conjunction with the document
- preparation tools of Isabelle described in \cite{isabelle-sys}.
+ preparation tools of Isabelle described in \chref{ch:document-prep}.
Thus partial or even wrong proof attempts can be discussed in a
logically sound manner. Note that the Isabelle {\LaTeX} macros can
be easily adapted to print something like ``@{text "\<dots>"}'' instead of
--- a/doc-src/IsarRef/Thy/ROOT.ML Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/IsarRef/Thy/ROOT.ML Tue Nov 18 18:25:10 2008 +0100
@@ -14,4 +14,5 @@
use_thy "Generic";
use_thy "HOL_Specific";
use_thy "Quick_Reference";
+use_thy "Symbols";
use_thy "ML_Tactic";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/Symbols.thy Tue Nov 18 18:25:10 2008 +0100
@@ -0,0 +1,49 @@
+(* $Id$ *)
+
+theory Symbols
+imports Pure
+begin
+
+chapter {* Standard Isabelle symbols \label{app:symbols} *}
+
+text {*
+ Isabelle supports an infinite number of non-ASCII symbols, which are
+ represented in source text as @{verbatim "\\"}@{verbatim "<"}@{text
+ name}@{verbatim ">"} (where @{text name} may be any identifier). It
+ is left to front-end tools how to present these symbols to the user.
+ The collection of predefined standard symbols given below is
+ available by default for Isabelle document output, due to
+ appropriate definitions of @{verbatim "\\"}@{verbatim isasym}@{text
+ name} for each @{verbatim "\\"}@{verbatim "<"}@{text name}@{verbatim
+ ">"} in the @{verbatim isabellesym.sty} file. Most of these symbols
+ are displayed properly in Proof~General if used with the X-Symbol
+ package.
+
+ Moreover, any single symbol (or ASCII character) may be prefixed by
+ @{verbatim "\\"}@{verbatim "<^sup>"}, for superscript and @{verbatim
+ "\\"}@{verbatim "<^sub>"}, for subscript, such as @{verbatim
+ "A\\"}@{verbatim "<^sup>\<star>"}, for @{text "A\<^sup>\<star>"} the alternative
+ versions @{verbatim "\\"}@{verbatim "<^isub>"} and @{verbatim
+ "\\"}@{verbatim "<^isup>"} are considered as quasi letters and may
+ be used within identifiers. Sub- and superscripts that span a
+ region of text are marked up with @{verbatim "\\"}@{verbatim
+ "<^bsub>"}@{text "\<dots>"}@{verbatim "\\"}@{verbatim "<^esub>"}, and
+ @{verbatim "\\"}@{verbatim "<^bsup>"}@{text "\<dots>"}@{verbatim
+ "\\"}@{verbatim "<^esup>"} respectively. Furthermore, all ASCII
+ characters and most other symbols may be printed in bold by
+ prefixing @{verbatim "\\"}@{verbatim "<^bold>"} such as @{verbatim
+ "\\"}@{verbatim "<^bold>\\"}@{verbatim "<alpha>"} for @{text
+ "\<^bold>\<alpha>"}. Note that @{verbatim "\\"}@{verbatim "<^bold>"}, may
+ \emph{not} be combined with sub- or superscripts for single symbols.
+
+ Further details of Isabelle document preparation are covered in
+ \chref{ch:document-prep}.
+
+ \begin{center}
+ \begin{isabellebody}
+ \input{syms}
+ \end{isabellebody}
+ \end{center}
+*}
+
+end
\ No newline at end of file
--- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Tue Nov 18 18:25:10 2008 +0100
@@ -186,8 +186,9 @@
symbols like this, although proper presentation is left to front-end
tools such as {\LaTeX} or Proof~General with the X-Symbol package.
A list of standard Isabelle symbols that work well with these tools
- is given in \cite[appendix~A]{isabelle-sys}. Note that \verb|\<lambda>| does not belong to the \isa{letter} category, since it is
- already used differently in the Pure term language.%
+ is given in \appref{app:symbols}. Note that \verb|\<lambda>| does
+ not belong to the \isa{letter} category, since it is already used
+ differently in the Pure term language.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/IsarRef/Thy/document/Proof.tex Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Tue Nov 18 18:25:10 2008 +0100
@@ -128,7 +128,7 @@
A typical application of \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} is to explain Isar proofs
\emph{within} the system itself, in conjunction with the document
- preparation tools of Isabelle described in \cite{isabelle-sys}.
+ preparation tools of Isabelle described in \chref{ch:document-prep}.
Thus partial or even wrong proof attempts can be discussed in a
logically sound manner. Note that the Isabelle {\LaTeX} macros can
be easily adapted to print something like ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' instead of
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/document/Symbols.tex Tue Nov 18 18:25:10 2008 +0100
@@ -0,0 +1,75 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Symbols}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Symbols\isanewline
+\isakeyword{imports}\ Pure\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Standard Isabelle symbols \label{app:symbols}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle supports an infinite number of non-ASCII symbols, which are
+ represented in source text as \verb|\|\verb|<|\isa{name}\verb|>| (where \isa{name} may be any identifier). It
+ is left to front-end tools how to present these symbols to the user.
+ The collection of predefined standard symbols given below is
+ available by default for Isabelle document output, due to
+ 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
+ are displayed properly in Proof~General if used with the X-Symbol
+ package.
+
+ Moreover, any single symbol (or ASCII character) may be prefixed by
+ \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
+ versions \verb|\|\verb|<^isub>| and \verb|\|\verb|<^isup>| are considered as quasi letters and may
+ be used within identifiers. Sub- and superscripts that span a
+ region of text are marked up with \verb|\|\verb|<^bsub>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esub>|, and
+ \verb|\|\verb|<^bsup>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esup>| respectively. Furthermore, all ASCII
+ characters and most other symbols may be printed in bold by
+ prefixing \verb|\|\verb|<^bold>| such as \verb|\|\verb|<^bold>\|\verb|<alpha>| for \isa{{\isachardoublequote}\isactrlbold {\isasymalpha}{\isachardoublequote}}. Note that \verb|\|\verb|<^bold>|, may
+ \emph{not} be combined with sub- or superscripts for single symbols.
+
+ Further details of Isabelle document preparation are covered in
+ \chref{ch:document-prep}.
+
+ \begin{center}
+ \begin{isabellebody}
+ \input{syms}
+ \end{isabellebody}
+ \end{center}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/doc-src/IsarRef/isar-ref.tex Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/IsarRef/isar-ref.tex Tue Nov 18 18:25:10 2008 +0100
@@ -2,7 +2,14 @@
%% $Id$
\documentclass[12pt,a4paper,fleqn]{report}
-\usepackage{latexsym,graphicx}
+\usepackage{amssymb}
+\usepackage[greek,english]{babel}
+\usepackage[latin1]{inputenc}
+\usepackage[only,bigsqcap]{stmaryrd}
+\usepackage{textcomp}
+\usepackage{latexsym}
+\usepackage{graphicx}
+\let\intorig=\int %iman.sty redefines \int
\usepackage{../iman,../extra,../isar,../proof}
\usepackage[nohyphen,strings]{../underscore}
\usepackage{../isabelle,../isabellesym}
@@ -89,6 +96,8 @@
\appendix
\input{Thy/document/Quick_Reference.tex}
+\let\int\intorig
+\input{Thy/document/Symbols.tex}
\input{Thy/document/ML_Tactic.tex}
\begingroup
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/showsymbols Tue Nov 18 18:25:10 2008 +0100
@@ -0,0 +1,28 @@
+#!/usr/bin/env perl
+#
+# $Id$
+
+print "\\begin{supertabular}{ll\@{\\qquad}ll}\n";
+
+$eol = "&";
+
+while (<ARGV>) {
+ if (m/^\\newcommand\{\\isasym([A-Za-z]+)\}/) {
+ print "\\verb,\\<$1>, & {\\isasym$1} $eol\n";
+# print "\\verb,\\<$1>, & \\isactrlbold{\\isasym$1}~{\\isasym$1} $eol\n";
+# print "\\verb,\\<$1>, & B\\isactrlsup{\\isasym$1} $eol\n";
+# print "\\verb,\\<$1>, & B\\isactrlsub{\\isasym$1} $eol\n";
+ if ("$eol" eq "&") {
+ $eol = "\\\\";
+ } else {
+ $eol = "&";
+ }
+ }
+}
+
+if ("$eol" eq "\\\\") {
+ print "$eol\n";
+}
+
+print "\\end{supertabular}\n";
+
--- a/doc-src/System/IsaMakefile Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/System/IsaMakefile Tue Nov 18 18:25:10 2008 +0100
@@ -22,7 +22,7 @@
Pure-System: $(LOG)/Pure-System.gz
$(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML \
- Thy/Basics.thy Thy/Misc.thy Thy/Presentation.thy Thy/Symbols.thy
+ Thy/Basics.thy Thy/Misc.thy Thy/Presentation.thy
@$(USEDIR) -s System Pure Thy
--- a/doc-src/System/Makefile Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/System/Makefile Tue Nov 18 18:25:10 2008 +0100
@@ -13,16 +13,12 @@
NAME = system
FILES = system.tex Thy/document/Basics.tex Thy/document/Misc.tex \
- Thy/document/Presentation.tex Thy/document/Symbols.tex \
- ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
-OUTPUT = syms.tex
-
-syms.tex: showsymbols ../isabellesym.sty
- @./showsymbols <../isabellesym.sty >syms.tex
+ Thy/document/Presentation.tex ../iman.sty ../extra.sty \
+ ../ttbox.sty ../manual.bib
dvi: $(NAME).dvi
-$(NAME).dvi: $(FILES) isabelle.eps syms.tex
+$(NAME).dvi: $(FILES) isabelle.eps
$(LATEX) $(NAME)
$(BIBTEX) $(NAME)
$(LATEX) $(NAME)
@@ -32,7 +28,7 @@
pdf: $(NAME).pdf
-$(NAME).pdf: $(FILES) isabelle.pdf syms.tex
+$(NAME).pdf: $(FILES) isabelle.pdf
$(PDFLATEX) $(NAME)
$(BIBTEX) $(NAME)
$(PDFLATEX) $(NAME)
--- a/doc-src/System/Thy/Presentation.thy Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/System/Thy/Presentation.thy Tue Nov 18 18:25:10 2008 +0100
@@ -686,8 +686,8 @@
"isabellesym.sty"} should be included as well. This package
contains a standard set of {\LaTeX} macro definitions @{verbatim
"\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim
- "<"}@{text foo}@{verbatim ">"}, (see \appref{app:symbols} for a
- complete list of predefined Isabelle symbols). Users may invent
+ "<"}@{text foo}@{verbatim ">"}, see \cite{isabelle-implementation} for a
+ complete list of predefined Isabelle symbols. Users may invent
further symbols as well, just by providing {\LaTeX} macros in a
similar fashion as in @{"file" "~~/lib/texinputs/isabellesym.sty"} of
the distribution.
--- a/doc-src/System/Thy/ROOT.ML Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/System/Thy/ROOT.ML Tue Nov 18 18:25:10 2008 +0100
@@ -7,4 +7,3 @@
use_thy "Basics";
use_thy "Presentation";
use_thy "Misc";
-use_thy "Symbols";
--- a/doc-src/System/Thy/Symbols.thy Tue Nov 18 18:22:49 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-(* $Id$ *)
-
-theory Symbols
-imports Pure
-begin
-
-chapter {* Standard Isabelle symbols \label{app:symbols} *}
-
-text {*
- Isabelle supports an infinite number of non-ASCII symbols, which are
- represented in source text as @{verbatim "\\"}@{verbatim "<"}@{text
- name}@{verbatim ">"} (where @{text name} may be any identifier). It
- is left to front-end tools how to present these symbols to the user.
- The collection of predefined standard symbols given below is
- available by default for Isabelle document output, due to
- appropriate definitions of @{verbatim "\\"}@{verbatim isasym}@{text
- name} for each @{verbatim "\\"}@{verbatim "<"}@{text name}@{verbatim
- ">"} in the @{verbatim isabellesym.sty} file. Most of these symbols
- are displayed properly in Proof~General if used with the X-Symbol
- package.
-
- Moreover, any single symbol (or ASCII character) may be prefixed by
- @{verbatim "\\"}@{verbatim "<^sup>"}, for superscript and @{verbatim
- "\\"}@{verbatim "<^sub>"}, for subscript, such as @{verbatim
- "A\\"}@{verbatim "<^sup>\<star>"}, for @{text "A\<^sup>\<star>"} the alternative
- versions @{verbatim "\\"}@{verbatim "<^isub>"} and @{verbatim
- "\\"}@{verbatim "<^isup>"} are considered as quasi letters and may
- be used within identifiers. Sub- and superscripts that span a
- region of text are marked up with @{verbatim "\\"}@{verbatim
- "<^bsub>"}@{text "\<dots>"}@{verbatim "\\"}@{verbatim "<^esub>"}, and
- @{verbatim "\\"}@{verbatim "<^bsup>"}@{text "\<dots>"}@{verbatim
- "\\"}@{verbatim "<^esup>"} respectively. Furthermore, all ASCII
- characters and most other symbols may be printed in bold by
- prefixing @{verbatim "\\"}@{verbatim "<^bold>"} such as @{verbatim
- "\\"}@{verbatim "<^bold>\\"}@{verbatim "<alpha>"} for @{text
- "\<^bold>\<alpha>"}. Note that @{verbatim "\\"}@{verbatim "<^bold>"}, may
- \emph{not} be combined with sub- or superscripts for single symbols.
-
- Further details of Isabelle document preparation are covered in
- \chref{ch:present}.
-
- \begin{center}
- \begin{isabellebody}
- \input{syms}
- \end{isabellebody}
- \end{center}
-*}
-
-end
\ No newline at end of file
--- a/doc-src/System/Thy/document/Presentation.tex Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/System/Thy/document/Presentation.tex Tue Nov 18 18:25:10 2008 +0100
@@ -694,8 +694,8 @@
If the text contains any references to Isabelle symbols (such as
\verb|\|\verb|<forall>|) then \verb|isabellesym.sty| should be included as well. This package
- 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
- complete list of predefined Isabelle symbols). Users may invent
+ 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
+ complete list of predefined Isabelle symbols. Users may invent
further symbols as well, just by providing {\LaTeX} macros in a
similar fashion as in \hyperlink{file.~~/lib/texinputs/isabellesym.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabellesym{\isachardot}sty}}}} of
the distribution.
--- a/doc-src/System/Thy/document/Symbols.tex Tue Nov 18 18:22:49 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Symbols}%
-%
-\isadelimtheory
-\isanewline
-\isanewline
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Symbols\isanewline
-\isakeyword{imports}\ Pure\isanewline
-\isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupchapter{Standard Isabelle symbols \label{app:symbols}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Isabelle supports an infinite number of non-ASCII symbols, which are
- represented in source text as \verb|\|\verb|<|\isa{name}\verb|>| (where \isa{name} may be any identifier). It
- is left to front-end tools how to present these symbols to the user.
- The collection of predefined standard symbols given below is
- available by default for Isabelle document output, due to
- 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
- are displayed properly in Proof~General if used with the X-Symbol
- package.
-
- Moreover, any single symbol (or ASCII character) may be prefixed by
- \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
- versions \verb|\|\verb|<^isub>| and \verb|\|\verb|<^isup>| are considered as quasi letters and may
- be used within identifiers. Sub- and superscripts that span a
- region of text are marked up with \verb|\|\verb|<^bsub>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esub>|, and
- \verb|\|\verb|<^bsup>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esup>| respectively. Furthermore, all ASCII
- characters and most other symbols may be printed in bold by
- prefixing \verb|\|\verb|<^bold>| such as \verb|\|\verb|<^bold>\|\verb|<alpha>| for \isa{{\isachardoublequote}\isactrlbold {\isasymalpha}{\isachardoublequote}}. Note that \verb|\|\verb|<^bold>|, may
- \emph{not} be combined with sub- or superscripts for single symbols.
-
- Further details of Isabelle document preparation are covered in
- \chref{ch:present}.
-
- \begin{center}
- \begin{isabellebody}
- \input{syms}
- \end{isabellebody}
- \end{center}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/System/showsymbols Tue Nov 18 18:22:49 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-#!/usr/bin/env perl
-#
-# $Id$
-
-print "\\begin{supertabular}{ll\@{\\qquad}ll}\n";
-
-$eol = "&";
-
-while (<ARGV>) {
- if (m/^\\newcommand\{\\isasym([A-Za-z]+)\}/) {
- print "\\verb,\\<$1>, & {\\isasym$1} $eol\n";
-# print "\\verb,\\<$1>, & \\isactrlbold{\\isasym$1}~{\\isasym$1} $eol\n";
-# print "\\verb,\\<$1>, & B\\isactrlsup{\\isasym$1} $eol\n";
-# print "\\verb,\\<$1>, & B\\isactrlsub{\\isasym$1} $eol\n";
- if ("$eol" eq "&") {
- $eol = "\\\\";
- } else {
- $eol = "&";
- }
- }
-}
-
-if ("$eol" eq "\\\\") {
- print "$eol\n";
-}
-
-print "\\end{supertabular}\n";
-
--- a/doc-src/System/system.tex Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/System/system.tex Tue Nov 18 18:25:10 2008 +0100
@@ -2,13 +2,7 @@
%% $Id$
\documentclass[12pt,a4paper]{report}
-\usepackage{amssymb}
-\usepackage[greek,english]{babel}
-\usepackage[latin1]{inputenc}
-\usepackage[only,bigsqcap]{stmaryrd}
-\usepackage{textcomp}
\usepackage{supertabular}
-\let\intorig=\int %iman.sty redefines \int
\usepackage{graphicx}
\usepackage{../iman,../extra,../isar,../ttbox}
\usepackage[nohyphen,strings]{../underscore}
@@ -36,13 +30,9 @@
\maketitle
\pagenumbering{roman} \tableofcontents \clearfirst
-\input{Thy/document/Basics}
-\input{Thy/document/Presentation}
-\input{Thy/document/Misc}
-
-\appendix
-\let\int\intorig
-\input{Thy/document/Symbols}
+\input{Thy/document/Basics.tex}
+\input{Thy/document/Presentation.tex}
+\input{Thy/document/Misc.tex}
\begingroup
\bibliographystyle{plain} \small\raggedright\frenchspacing
--- a/doc-src/TutorialI/Datatype/document/Nested.tex Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex Tue Nov 18 18:25:10 2008 +0100
@@ -119,7 +119,7 @@
its definition is found in theorem \isa{o{\isacharunderscore}def}).
\end{exercise}
\begin{exercise}\label{ex:trev-trev}
- 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}
+ 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}
that recursively reverses the order of arguments of all function symbols in a
term. Prove that \isa{trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t}.
\end{exercise}
--- a/doc-src/TutorialI/Documents/Documents.thy Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/TutorialI/Documents/Documents.thy Tue Nov 18 18:25:10 2008 +0100
@@ -107,7 +107,7 @@
\verb,\,\verb,<forall>, symbol as~@{text \<forall>}.
A list of standard Isabelle symbols is given in
- \cite[appendix~A]{isabelle-sys}. You may introduce your own
+ \cite{isabelle-isar-ref}. You may introduce your own
interpretation of further symbols by configuring the appropriate
front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
macros (see also \S\ref{sec:doc-prep-symbols}). There are also a
@@ -666,7 +666,7 @@
straightforward generalization of ASCII characters. While Isabelle
does not impose any interpretation of the infinite collection of
named symbols, {\LaTeX} documents use canonical glyphs for certain
- standard symbols \cite[appendix~A]{isabelle-sys}.
+ standard symbols \cite{isabelle-isar-ref}.
The {\LaTeX} code produced from Isabelle text follows a simple
scheme. You can tune the final appearance by redefining certain
--- a/doc-src/TutorialI/Documents/document/Documents.tex Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Tue Nov 18 18:25:10 2008 +0100
@@ -123,7 +123,7 @@
\verb,\,\verb,<forall>, symbol as~\isa{{\isasymforall}}.
A list of standard Isabelle symbols is given in
- \cite[appendix~A]{isabelle-sys}. You may introduce your own
+ \cite{isabelle-isar-ref}. You may introduce your own
interpretation of further symbols by configuring the appropriate
front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
macros (see also \S\ref{sec:doc-prep-symbols}). There are also a
@@ -394,18 +394,18 @@
(usually rooted at \verb,~/isabelle/browser_info,).
\medskip The easiest way to manage Isabelle sessions is via
- \texttt{isatool mkdir} (generates an initial session source setup)
- and \texttt{isatool make} (run sessions controlled by
+ \texttt{isabelle mkdir} (generates an initial session source setup)
+ and \texttt{isabelle make} (run sessions controlled by
\texttt{IsaMakefile}). For example, a new session
\texttt{MySession} derived from \texttt{HOL} may be produced as
follows:
\begin{verbatim}
- isatool mkdir HOL MySession
- isatool make
+ isabelle mkdir HOL MySession
+ isabelle make
\end{verbatim}
- The \texttt{isatool make} job also informs about the file-system
+ The \texttt{isabelle make} job also informs about the file-system
location of the ultimate results. The above dry run should be able
to produce some \texttt{document.pdf} (with dummy title, empty table
of contents etc.). Any failure at this stage usually indicates
@@ -441,7 +441,7 @@
several sessions may be managed by the same \texttt{IsaMakefile}.
See the \emph{Isabelle System Manual} \cite{isabelle-sys}
for further details, especially on
- \texttt{isatool usedir} and \texttt{isatool make}.
+ \texttt{isabelle usedir} and \texttt{isabelle make}.
\end{itemize}
@@ -464,7 +464,7 @@
\texttt{MySession/document} directory as well. In particular,
adding a file named \texttt{root.bib} causes an automatic run of
\texttt{bibtex} to process a bibliographic database; see also
- \texttt{isatool document} \cite{isabelle-sys}.
+ \texttt{isabelle document} \cite{isabelle-sys}.
\medskip Any failure of the document preparation phase in an
Isabelle batch session leaves the generated sources in their target
@@ -741,7 +741,7 @@
straightforward generalization of ASCII characters. While Isabelle
does not impose any interpretation of the infinite collection of
named symbols, {\LaTeX} documents use canonical glyphs for certain
- standard symbols \cite[appendix~A]{isabelle-sys}.
+ standard symbols \cite{isabelle-isar-ref}.
The {\LaTeX} code produced from Isabelle text follows a simple
scheme. You can tune the final appearance by redefining certain
@@ -844,7 +844,7 @@
tagged region, in order to keep, drop, or fold the corresponding
parts of the document. See the \emph{Isabelle System Manual}
\cite{isabelle-sys} for further details, especially on
- \texttt{isatool usedir} and \texttt{isatool document}.
+ \texttt{isabelle usedir} and \texttt{isabelle document}.
Ignored material is specified by delimiting the original formal
source with special source comments
--- a/doc-src/TutorialI/Types/document/Numbers.tex Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Tue Nov 18 18:25:10 2008 +0100
@@ -569,9 +569,7 @@
effect of show sorts on the above
\begin{isabelle}%
-{\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
-\isaindent{{\isacharparenleft}}c\ {\isacharasterisk}\ {\isacharparenleft}b{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
-{\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
+{\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}%
\end{isabelle}
\rulename{mult_cancel_left}%
\end{isamarkuptext}%