Revision: 5905
http://hol.svn.sourceforge.net/hol/?rev=5905&view=rev
Author: acjf3
Date: 2008-04-29 02:00:05 -0700 (Tue, 29 Apr 2008)
Log Message:
-----------
Have "modernised" the manuals.
1. By default it now uses pdflatex. Postscript can still be generated
with "make ps".
* Authors should not use pstricks - it doesn't work with pdflatex.
* The commuting diagrams in the tutorial have been redone with
XP-pic -- with much less code.
* Other figures can be included with "\includegraphics", which is provided
by the graphicx package. Just make sure you upload EPS and PDF versions
of the diagrams.
* The Covers directory and old logos have been removed -- they weren't
maintainable. (Have tarted up the title.tex pages.)
2. The make files have been updated and cleaned up. There is
now "make clean" option in $HOLDIR/Manuals.
* As a side note, I noticed that a call to "make" in $HOLDIR/Manuals didn't
do anything on Mac OS X. I had to do "make -B".
3. Have eliminated font substitution errors.
* Don't include the charter.sty package - the font is now changed
in LaTeX/layout.sty. This avoids changing the \tt font, which
causes problems with \section{\texttt{stuff}}.
* Left and right braces in \tt font can be a problem. \{ and \} give
maths font, which is fine in places. \verb%{}% will work but
\verb can't be used in certain places (inside another command).
Have added \lb and \rb to LaTeX/commands.tex. These are just
\char'173 and \char'175 and can be used anywhere.
4. Have commented out the mucking about with page numbering.
* This means that if you do a goto page N (in Acrobat, Preview.app etc.)
then you go to page N of the main text. (Stops folks having to add
an offset to entries in the index.)
5. Have made things more compatible with amsmath.
* The environment "boxed" (LaTeX/commands.tex) has been renamed to "holboxed".
* Have changed "\over" to "\frac".
* amsmath is turned on in the Logic manual, mainly to get text subscripts
typesetting better.
6. Have removed a bunch of hbox (and other) warnings.
* Don't do "\begin{session}\begin{hol}\begin{verbatim}...", do
"\begin{session}\begin{verbatim}..." instead.
* Don't use "\begin{hol}\begin{verbatim}..." is item lists.
Instead just do "\begin{verbatim}".
* Have done some small text edits - hopefully these are okay.
* A few more warnings remain and there's not much that can be done
about underfull vboxes -- short of going with "\raggedbottom".
7. Have made Doc2TeX and reference.tex used fancyvrb, This means the
font size can be set to \small globally. Have also removed the
\samepage directive -- a few bad breaks are better than having
material bigger than the size of the page.
Modified Paths:
--------------
HOL/Manual/Description/HolBdd.tex
HOL/Manual/Description/Makefile
HOL/Manual/Description/conv.tex
HOL/Manual/Description/definitions.tex
HOL/Manual/Description/description.tex
HOL/Manual/Description/drules.tex
HOL/Manual/Description/holCheck.tex
HOL/Manual/Description/libraries.tex
HOL/Manual/Description/misc.tex
HOL/Manual/Description/system.tex
HOL/Manual/Description/tactics.tex
HOL/Manual/Description/theories.tex
HOL/Manual/Description/title.tex
HOL/Manual/Description/version2.tex
HOL/Manual/Guide/guide.tex
HOL/Manual/LaTeX/commands.tex
HOL/Manual/LaTeX/layout.sty
HOL/Manual/Logic/Makefile
HOL/Manual/Logic/logic.tex
HOL/Manual/Logic/semantics.tex
HOL/Manual/Logic/syntax.tex
HOL/Manual/Logic/title.tex
HOL/Manual/Makefile
HOL/Manual/Quick/Makefile
HOL/Manual/Quick/quick.tex
HOL/Manual/READ-ME
HOL/Manual/Reference/Makefile
HOL/Manual/Reference/reference.tex
HOL/Manual/Reference/title.tex
HOL/Manual/Tutorial/Makefile
HOL/Manual/Tutorial/combin.tex
HOL/Manual/Tutorial/euclid.tex
HOL/Manual/Tutorial/intro.tex
HOL/Manual/Tutorial/logic.tex
HOL/Manual/Tutorial/preface.tex
HOL/Manual/Tutorial/proof-tools.tex
HOL/Manual/Tutorial/title.tex
HOL/Manual/Tutorial/tutorial.tex
HOL/help/Docfiles/Conv.ORELSEC.doc
HOL/help/src/Doc2Tex.sml
Added Paths:
-----------
HOL/Manual/Description/figs/asr.pdf
HOL/Manual/Description/figs/bits.pdf
HOL/Manual/Description/figs/concat.pdf
HOL/Manual/Description/figs/ex.pdf
HOL/Manual/Description/figs/lsl.pdf
HOL/Manual/Description/figs/lsr.pdf
HOL/Manual/Description/figs/reverse.pdf
HOL/Manual/Description/figs/ror.pdf
HOL/Manual/Description/figs/rrx.pdf
HOL/Manual/Logo/lantern.eps
HOL/Manual/Logo/lantern.pdf
Removed Paths:
-------------
HOL/Manual/Covers/
HOL/Manual/Description/underscore.sty
HOL/Manual/LaTeX/cover_info.tex
HOL/Manual/Logo/Makefile
HOL/Manual/Logo/logo.eps
HOL/Manual/Logo/logo.gif
HOL/Manual/Logo/logo.ico
HOL/Manual/Logo/logo.obj
Modified: HOL/Manual/Description/HolBdd.tex
===================================================================
--- HOL/Manual/Description/HolBdd.tex 2008-04-29 07:07:14 UTC (rev 5904)
+++ HOL/Manual/Description/HolBdd.tex 2008-04-29 09:00:05 UTC (rev 5905)
@@ -1,31 +1,23 @@
-\documentclass[12pt]{book}
-
-\usepackage{alltt}
-\usepackage{epsfig}
-\usepackage{pstricks}
+\documentclass[12pt,fleqn]{book}
\usepackage{makeidx}
\usepackage{url}
\usepackage{index}
\usepackage{multind}
\usepackage{fancyvrb}
-\usepackage{charter}
\usepackage{latexsym}
-%\usepackage{amsmath}
+%\usepackage{amsmath}
\usepackage{amssymb}
-%\usepackage{amsbsy}
-%\usepackage{amsthm}
-\usepackage{makeidx}
-\usepackage{fleqn}
+%\usepackage{amsbsy}
\usepackage{alltt}
\usepackage{../LaTeX/layout}
\usepackage{graphicx}
-%\usepackage{pst-node}
-\usepackage{epsfig}
-\usepackage{url}
+\input{../LaTeX/commands}
+
\makeindex
\newcommand{\hbc}[2]{
+\addtolength{\minipagewidth}{-10pt}
\begin{minipage}{\minipagewidth}
\begin{footnotesize}
{\texttt{#1}}
@@ -82,8 +74,6 @@
%\parindent 0mm
%\parskip 1mm
-\input{../LaTeX/commands}
-
\setcounter{sessioncount}{0}
%\title{HolBddLib}
%\date{}
@@ -170,7 +160,7 @@
judgements $\termbdd{a}{\rho}{t}{b}$ analogously
to the way the type $\ty{thm}$ models theorems $\vdash t$.
-\t{HolBddLib} currently contains two main structures: \t{PrimitiveBddRules}
+The structure \t{HolBddLib} currently contains two main structures: \t{PrimitiveBddRules}
which defines a protected type \termbddty and rules for generating
values of this type, and \t{DerivedBddRules} that contains derived
rules for performing simple fixed-point calculations. There is also a
@@ -536,7 +526,7 @@
restrict : bdd -> assignment -> bdd
\end{verbatim}\index{HolBddLib!ML bindings!{restrict}@\ml{restrict}}\index{HolBddLib!ML bindings!{assignment}@\ml{assignment}}\index{HolBddLib!ML bindings!{getAssignment}@\ml{getAssignment}}
-Evaluating \t{assignment[($v_1$,$t_1$), $\ldots$ , ($v_n$,$t_n$)]}
+\noindent Evaluating \t{assignment[($v_1$,$t_1$), $\ldots$ , ($v_n$,$t_n$)]}
creates an assignment specifying that each $v_i$ be instantiated to
$\t{fromBool(}t_i\t{)}$ (for $1{\leq}i{\leq}n$).
@@ -838,7 +828,7 @@
the following Postscript diagram of a BDD
\begin{center}
-\epsfig{file=figs/ex.ps, height=5cm, width=3cm}
+\includegraphics[width=3cm, height=5cm]{figs/ex}
\end{center}
\subsubsection{Dynamic variable reordering}\index{HolBddLib!BDD!dynamic reordering}
@@ -994,7 +984,7 @@
often denoted by $\rho$,
from HOL variables to BDD variables;
-\item \t{PrintBdd} provides rudimentary facilities for printing
+\item \t{PrintBdd} provides some rudimentary facilities for printing
BDDs with respect to a varmap;
\item \t{PrimitiveBddRules} defines the protected type \termbddty
@@ -1203,7 +1193,7 @@
$\termbdd{}{\rho}{t}{b}$.
-\paragraph{Extending and contracting the varmap} {\(\)}\\
+\subsubsection*{Extending and contracting the varmap}
\newsavebox\BddExtendVarmap
\begin{lrbox}\BddExtendVarmap
@@ -1219,7 +1209,7 @@
\vspace*{-2mm}
$$\begin{array}{c}
-{\footnotesize\t{Varmap.extends}}~\rho_1~\rho_2 \qquad \termbdd{a}{\rho_1}{t}{b}
+{\t{\footnotesize Varmap.extends}}~\rho_1~\rho_2 \qquad \termbdd{a}{\rho_1}{t}{b}
\\ \hline
\termbdd{a}{\rho_2}{t}{b}
\end{array}$$
@@ -1236,7 +1226,7 @@
\bigskip
\newsavebox\BddFreevarsContractVarmap
-\begin{lrbox}\BddFreevarsContractVarmap
+\noindent\begin{lrbox}\BddFreevarsContractVarmap
\begin{minipage}{\minipagewidth}
\begin{footnotesize}
@@ -1251,7 +1241,7 @@
$$\begin{array}{c}
\termbdd{a}{\rho}{t}{b} \qquad \mbox{$v$ not free in $t$}
\\ \hline
-\termbdd{a}{({\footnotesize{\texttt{Varmap.remove~"}}}v{\footnotesize{\texttt{"}}}~\rho)}{t}{b}
+\termbdd{a}{({\texttt{\footnotesize{Varmap.remove~"}}}v{\texttt{\footnotesize{"}}}~\rho)}{t}{b}
\end{array}$$
\noindent \rule\minipagewidth{0.1pt}
@@ -1268,7 +1258,7 @@
\bigskip
\newsavebox\BddSupportContractVarmap
-\begin{lrbox}\BddSupportContractVarmap
+\noindent\begin{lrbox}\BddSupportContractVarmap
\begin{minipage}{\minipagewidth}
\begin{footnotesize}
@@ -1283,7 +1273,7 @@
$$\begin{array}{c}
\termbdd{a}{\rho}{t}{b} \qquad \mbox{$\rho(v)$ doesn't occur in $b$}
\\ \hline
-\termbdd{a}{({\footnotesize{\texttt{Varmap.remove~"}}}v{\footnotesize{\texttt{"}}}~\rho)}{t}{b}
+\termbdd{a}{({\texttt{\footnotesize{Varmap.remove~"}}}v{\texttt{\footnotesize{"}}}~\rho)}{t}{b}
\end{array}$$
\noindent \rule\minipagewidth{0.1pt}
@@ -1296,7 +1286,7 @@
\fbox{\usebox{\BddSupportContractVarmap}}\index{HolBddLib!ML bindings!{BddSupportContractVarmap}@\ml{BddSupportContractVarmap}}
-\paragraph{Variables and constants}{\(\)}\\
+\subsubsection*{Variables and constants}
\newsavebox\BddVar
\begin{lrbox}\BddVar
@@ -1315,16 +1305,16 @@
\begin{array}{c}
\rho(v)=n
\\ \hline
-\termbdd{}{\rho}{v}{{\footnotesize\t{ithvar}}~n}
-\end{array} ~\footnotesize{\t{BddVar~true}}
+\termbdd{}{\rho}{v}{{\t{\footnotesize ithvar}}~n}
+\end{array} ~{\t{\footnotesize BddVar~true}}
\\[8mm]
\begin{array}{c}
\rho(v)=n
\\ \hline
-\termbdd{}{\rho}{\neg v}{{\footnotesize\t{nithvar}}~n}
-\end{array}~ {\footnotesize\t{BddVar~false}}
+\termbdd{}{\rho}{\neg v}{{\t{\footnotesize nithvar}}~n}
+\end{array}~ {\t{\footnotesize BddVar~false}}
\end{array}$$
@@ -1340,7 +1330,7 @@
\bigskip
\newsavebox\BddCon
-\begin{lrbox}\BddCon
+\noindent\begin{lrbox}\BddCon
\begin{minipage}{\minipagewidth}
\begin{footnotesize}
@@ -1356,15 +1346,15 @@
\begin{array}{c}
\\ \hline
-\termbdd{}{\rho}{{\footnotesize\t{T}}}{{\footnotesize\t{TRUE}}}
-\end{array} ~\footnotesize{\t{BddCon~true}}
+\termbdd{}{\rho}{{\t{\footnotesize T}}}{{\t{\footnotesize TRUE}}}
+\end{array} ~{\t{\footnotesize BddCon~true}}
\\[8mm]
\begin{array}{c}
\\ \hline
-\termbdd{}{\rho}{{\footnotesize\t{F}}}{{\footnotesize\t{FALSE}}}
-\end{array}~ {\footnotesize\t{BddCon~false}}
+\termbdd{}{\rho}{{\t{\footnotesize F}}}{{\t{\footnotesize FALSE}}}
+\end{array}~ {\t{\footnotesize BddCon~false}}
\end{array}$$
@@ -1377,7 +1367,7 @@
\end{lrbox}
\fbox{\usebox{\BddCon}}\index{HolBddLib!ML bindings!{BddCon}@\ml{BddCon}}
-\paragraph{Boolean operations}{\(\)}\\
+\subsubsection*{Boolean operations}
@@ -1397,7 +1387,7 @@
$$\begin{array}{c}
\termbdd{a}{\rho}{t}{b}
\\ \hline
-\termbdd{a}{\rho}{\neg t}{{\footnotesize\t{NOT}}~b}
+\termbdd{a}{\rho}{\neg t}{{\t{\footnotesize NOT}}~b}
\end{array}$$
\noindent \rule\minipagewidth{0.1pt}
@@ -1412,7 +1402,7 @@
\bigskip
\newsavebox\BddIte
-\begin{lrbox}\BddIte
+\noindent\begin{lrbox}\BddIte
\begin{minipage}{\minipagewidth}
\begin{footnotesize}
@@ -1427,13 +1417,13 @@
$$\begin{array}{c}
\termbdd{a}{\rho}{t}{b} \qquad \termbdd{a_1}{\rho}{t_1}{b_1} \qquad \termbdd{a_2}{\rho}{t_2}{b_2}
\\ \hline
-\termbdd{a \cup a_1 \cup a_2}{\rho}{\mbox{\footnotesize\t{(if~$t$~then~$t_1$~else~$t_2$)}}}{{\footnotesize\t{ITE}}~b~b_1~b_2}
+\termbdd{a \cup a_1 \cup a_2}{\rho}{\mbox{\t{\footnotesize (if~$t$~then~$t_1$~else~$t_2$)}}}{{\t{\footnotesize ITE}}~b~b_1~b_2}
\end{array}$$
\noindent \rule\minipagewidth{0.1pt}
\begin{footnotesize}
-Raises {\footnotesize\t{BddIteError}} if the varmaps of the hypotheses are not all
+Raises {\t{\footnotesize BddIteError}} if the varmaps of the hypotheses are not all
pointer equal
\end{footnotesize}
\end{minipage}
@@ -1444,7 +1434,7 @@
\bigskip
\newsavebox\BddOp
-\begin{lrbox}\BddOp
+\noindent\begin{lrbox}\BddOp
\begin{minipage}{\minipagewidth}
\begin{footnotesize}
@@ -1459,7 +1449,7 @@
$$\begin{array}{c}
\termbdd{a_1}{\rho}{t_1}{b_1} \qquad \termbdd{a_2}{\rho}{t_2}{b_2}
\\ \hline
-\termbdd{a_1\cup a_2}{\rho}{{\footnotesize\t{(termApply}}~t_1~t_2~bddop{\footnotesize\t{)}}}{{\footnotesize\t{apply}}~b_1~b_2~bddop}
+\termbdd{a_1\cup a_2}{\rho}{{\t{\footnotesize (termApply}}~t_1~t_2~bddop{\t{\footnotesize )}}}{{\t{\footnotesize apply}}~b_1~b_2~bddop}
\end{array}$$
\noindent \rule\minipagewidth{0.1pt}
@@ -1469,14 +1459,14 @@
the HOL operation
corresponding to the \Buddy{} BDD operation $bddop$ to terms $t_1$ and $t_2$
(see Section~\ref{misc}). The exception
-{\footnotesize\t{BddOpError}} is raised if the varmaps of the hypotheses are not pointer equal
+{\t{\footnotesize BddOpError}} is raised if the varmaps of the hypotheses are not pointer equal
\end{footnotesize}
\end{minipage}
\end{lrbox}
\fbox{\usebox{\BddOp}}\index{HolBddLib!ML bindings!{BddOp}@\ml{BddOp}}
-\paragraph{Quantification}{\(\)}\\
+\subsubsection*{Quantification}
\newsavebox\BddForall
\begin{lrbox}\BddForall
@@ -1494,8 +1484,8 @@
$$\begin{array}{c}
\termbdd{a}{\rho}{t}{b} \qquad \rho(v_1)=n_1,~ $\ldots$~,~ \rho(v_i)=n_i
\\ \hline
-\termbdd{a}{\rho}{({\footnotesize\forall} v_1~\cdots~v_i.~t)}%
-{{\footnotesize\t{forall~(makeset[}}n_1,\ldots,n_i{\footnotesize\t{])}}~b}
+\termbdd{a}{\rho}{({\scriptstyle\forall} v_1~\cdots~v_i.~t)}%
+{{\t{\footnotesize forall~(makeset[}}n_1,\ldots,n_i{\t{\footnotesize ])}}~b}
\end{array}$$
\noindent \rule\minipagewidth{0.1pt}
@@ -1513,7 +1503,7 @@
\newsavebox\BddExists
-\begin{lrbox}\BddExists
+\noindent\begin{lrbox}\BddExists
\begin{minipage}{\minipagewidth}
\begin{footnotesize}
@@ -1528,8 +1518,8 @@
$$\begin{array}{c}
\termbdd{a}{\rho}{t}{b} \qquad \rho(v_1)=n_1,~ $\ldots$~,~ \rho(v_i)=n_i
\\ \hline
-\termbdd{a}{\rho}{({\footnotesize\exists} v_1~\cdots~v_i.~t)}%
-{{\footnotesize\t{exist~(makeset[}}n_1,\ldots,n_i{\footnotesize\t{])}}~b}
+\termbdd{a}{\rho}{({\scriptstyle\exists} v_1~\cdots~v_i.~t)}%
+{{\t{\footnotesize exist~(makeset[}}n_1,\ldots,n_i{\t{\footnotesize ])}}~b}
\end{array}$$
\noindent \rule\minipagewidth{0.1pt}
@@ -1547,7 +1537,7 @@
\newsavebox\BddAppall
-\begin{lrbox}\BddAppall
+\noindent\begin{lrbox}\BddAppall
\begin{minipage}{\minipagewidth}
\begin{footnotesize}
@@ -1565,11 +1555,11 @@
\begin{array}{l}
{a_1 \cup a_2}%
~{\rho}%
-~{({\footnotesize\forall} v_1~\cdots~v_i.~%
-{\footnotesize\t{termApply}}~t_1~t_2~bddop)}\\
+~{({\scriptstyle\forall} v_1~\cdots~v_i.~%
+{\t{\footnotesize termApply}}~t_1~t_2~bddop)}\\
\mapsto\\
-{{\footnotesize\t{appall}}~b_1~b_2~bddop~%
-{\footnotesize\t{(makeset[}}n_1,\ldots,n_i{\footnotesize\t{])}}~b}
+{{\t{\footnotesize appall}}~b_1~b_2~bddop~%
+{\t{\footnotesize (makeset[}}n_1,\ldots,n_i{\t{\footnotesize ])}}~b}
\end{array}
\end{array}$$
@@ -1590,7 +1580,7 @@
\newsavebox\BddAppex
-\begin{lrbox}\BddAppex
+\noindent\begin{lrbox}\BddAppex
\begin{minipage}{\minipagewidth}
\begin{footnotesize}
@@ -1608,11 +1598,11 @@
\begin{array}{l}
{a_1 \cup a_2}%
~{\rho}%
-~{({\footnotesize\exists} v_1~\cdots~v_i.~%
-{\footnotesize\t{termApply}}~t_1~t_2~bddop)}\\
+~{({\scriptstyle\exists} v_1~\cdots~v_i.~%
+{\t{\footnotesize termApply}}~t_1~t_2~bddop)}\\
\mapsto\\
-{{\footnotesize\t{appex}}~b_1~b_2~bddop~%
-{\footnotesize\t{(makeset[}}n_1,\ldots,n_i{\footnotesize\t{])}}~b}
+{{\t{\footnotesize appex}}~b_1~b_2~bddop~%
+{\t{\footnotesize (makeset[}}n_1,\ldots,n_i{\t{\footnotesize ])}}~b}
\end{array}
\end{array}$$
@@ -1628,7 +1618,7 @@
\end{lrbox}
\fbox{\usebox{\BddAppex}}\index{HolBddLib!ML bindings!{BddAppex}@\ml{BddAppex}}
-\paragraph{Composition, repacement and restriction}{\(\)}\\
+\subsubsection*{Composition, repacement and restriction}
\newsavebox\BddCompose
@@ -1650,8 +1640,8 @@
\\ \hline
\termbdd{a_1 \cup a_2 \cup a}
{\rho}
-{(\mbox{\footnotesize\t{subst[$v_1$ |-> $t_1$] $t$}})}
-{\mbox{\footnotesize\t{compose(var $b_1$, $b_1'$) $b$}}}
+{(\mbox{\t{\footnotesize subst[$v_1$ |-> $t_1$] $t$}})}
+{\mbox{\t{\footnotesize compose(var $b_1$, $b_1'$) $b$}}}
\end{array}$$
\noindent \rule\minipagewidth{0.1pt}
@@ -1667,7 +1657,7 @@
\bigskip
\newsavebox\BddListCompose
-\begin{lrbox}\BddListCompose
+\noindent\begin{lrbox}\BddListCompose
\begin{minipage}{\minipagewidth}
\begin{footnotesize}
@@ -1681,18 +1671,18 @@
$$\begin{array}{c}
\begin{array}{l}
-{\footnotesize\t{[}} (\termbdd{a_1}{\rho}{v_1}{b_1},~~ \termbdd{a_1'}{\rho}{t_1}{b_1'}), \\
-\phantom{{\footnotesize\t{[}}(\termbdd{a_1}{\rho}{v_1}{b_1}} \vdots\\
-\phantom{{\footnotesize\t{[}}}(\termbdd{a_i}{\rho}{v_i}{b_i},~~~~ \termbdd{a_i'}{\rho}{t_i}{b_i'}){\footnotesize\t{]}}
+{\t{\footnotesize [}} (\termbdd{a_1}{\rho}{v_1}{b_1},~~ \termbdd{a_1'}{\rho}{t_1}{b_1'}), \\
+\phantom{{\t{\footnotesize [}}(\termbdd{a_1}{\rho}{v_1}{b_1}} \vdots\\
+\phantom{{\t{\footnotesize [}}}(\termbdd{a_i}{\rho}{v_i}{b_i},~~~~ \termbdd{a_i'}{\rho}{t_i}{b_i'}){\t{\footnotesize ]}}
\qquad \termbdd{a}{\rho}{t}{b}
\end{array}
\\ \hline
\begin{array}{l}
{a_1 \cup a_1'~\cup~\cdots~\cup~a_i \cup a_i' \cup a}\\
{\rho}\\
-{\mbox{\footnotesize\t{subst[$v_1$ |-> $t_1$,~$\ldots$~,~$v_i$ |-> $t_i$] $t$}}}\\
+{\mbox{\t{\footnotesize subst[$v_1$ |-> $t_1$,~$\ldots$~,~$v_i$ |-> $t_i$] $t$}}}\\
\mapsto\\
-{\mbox{\footnotesize\t{veccompose(composeSet[(var $b_1$, $b_1'$),~$\ldots$~,~(var $b_i$, $b_i'$)])$b$}}}
+{\mbox{\t{\footnotesize veccompose(composeSet[(var $b_1$, $b_1'$),~$\ldots$~,~(var $b_i$, $b_i'$)])$b$}}}
\end{array}
\end{array}$$
@@ -1710,7 +1700,7 @@
\bigskip
\newsavebox\BddRestrict
-\begin{lrbox}\BddRestrict
+\noindent\begin{lrbox}\BddRestrict
\begin{minipage}{\minipagewidth}
\begin{footnotesize}
@@ -1724,18 +1714,18 @@
$$\begin{array}{c}
\begin{array}{l}
-{\footnotesize\t{[}} (\termbdd{a_1}{\rho}{v_1}{b_1},~~ \termbdd{a_1'}{\rho}{c_1}{b_1'}), \\
-\phantom{{\footnotesize\t{[}}(\termbdd{a_1}{\rho}{v_1}{b_1}} \vdots\\
-\phantom{{\footnotesize\t{[}}}(\termbdd{a_i}{\rho}{v_i}{b_i},~~~~ \termbdd{a_i'}{\rho}{c_i}{b_i'}){\footnotesize\t{]}}
+{\t{\footnotesize [}} (\termbdd{a_1}{\rho}{v_1}{b_1},~~ \termbdd{a_1'}{\rho}{c_1}{b_1'}), \\
+\phantom{{\t{\footnotesize [}}(\termbdd{a_1}{\rho}{v_1}{b_1}} \vdots\\
+\phantom{{\t{\footnotesize [}}}(\termbdd{a_i}{\rho}{v_i}{b_i},~~~~ \termbdd{a_i'}{\rho}{c_i}{b_i'}){\t{\footnotesize ]}}
\qquad \termbdd{a}{\rho}{t}{b}
\end{array}
\\ \hline
\begin{array}{l}
{a_1 \cup a_1'~\cup~\cdots~\cup~a_i \cup a_i' \cup a}\\
{\rho}\\
-{\mbox{\footnotesize\t{subst[$v_1$ |-> $c_1$,~$\ldots$~,~$v_i$ |-> $c_i$] $t$}}}\\
+{\mbox{\t{\footnotesize subst[$v_1$ |-> $c_1$,~$\ldots$~,~$v_i$ |-> $c_i$] $t$}}}\\
\mapsto\\
-{\mbox{\footnotesize\t{restrict~$b$~(assignment[(var $b_1$, $\hat{c_1}$),~$\ldots$~,~(var $b_i$, $\hat{c_i}$)])}}}
+{\mbox{\t{\footnotesize restrict~$b$~(assignment[(var $b_1$, $\hat{c_1}$),~$\ldots$~,~(var $b_i$, $\hat{c_i}$)])}}}
\end{array}
\end{array}$$
@@ -1757,7 +1747,7 @@
\bigskip
\newsavebox\BddReplace
-\begin{lrbox}\BddReplace
+\noindent\begin{lrbox}\BddReplace
\begin{minipage}{\minipagewidth}
\begin{footnotesize}
@@ -1771,18 +1761,18 @@
$$\begin{array}{c}
\begin{array}{l}
-{\footnotesize\t{[}} (\termbdd{a_1}{\rho}{v_1}{b_1},~~ \termbdd{a_1'}{\rho}{v_1'}{b_1'}), \\
-\phantom{{\footnotesize\t{[}}(\termbdd{a_1}{\rho}{v_1}{b_1}} \vdots\\
-\phantom{{\footnotesize\t{[}}}(\termbdd{a_i}{\rho}{v_i}{b_i},~~~~ \termbdd{a_i'}{\rho}{v_i'}{b_i'}){\footnotesize\t{]}}
+{\t{\footnotesize [}} (\termbdd{a_1}{\rho}{v_1}{b_1},~~ \termbdd{a_1'}{\rho}{v_1'}{b_1'}), \\
+\phantom{{\t{\footnotesize [}}(\termbdd{a_1}{\rho}{v_1}{b_1}} \vdots\\
+\phantom{{\t{\footnotesize [}}}(\termbdd{a_i}{\rho}{v_i}{b_i},~~~~ \termbdd{a_i'}{\rho}{v_i'}{b_i'}){\t{\footnotesize ]}}
\qquad \termbdd{a}{\rho}{t}{b}
\end{array}
\\ \hline
\begin{array}{l}
{a_1 \cup a_1'~\cup~\cdots~\cup~a_i \cup a_i' \cup a}\\
{\rho}\\
-{\mbox{\footnotesize\t{subst[$v_1$ |-> $v_1'$,~$\ldots$~,~$v_i$ |-> $v_i'$] $t$}}}\\
+{\mbox{\t{\footnotesize subst[$v_1$ |-> $v_1'$,~$\ldots$~,~$v_i$ |-> $v_i'$] $t$}}}\\
\mapsto\\
-{\mbox{\footnotesize\t{replace~$b$~(makepairSet[(var $b_1$, var $b_1'$),~$\ldots$~,~(var $b_i$, var $b_i'$)])}}}
+{\mbox{\t{\footnotesize replace~$b$~(makepairSet[(var $b_1$, var $b_1'$),~$\ldots$~,~(var $b_i$, var $b_i'$)])}}}
\end{array}
\end{array}$$
@@ -1797,7 +1787,7 @@
\end{lrbox}
\fbox{\usebox{\BddReplace}}\index{HolBddLib!ML bindings!{BddReplace}@\ml{BddReplace}}
-\paragraph{Coudert, Berthet \& Madre simplification}\label{BddSimplify}{\(\)}\\
+\subsubsection*{Coudert, Berthet \& Madre simplification}\label{BddSimplify}
\vspace*{-1mm}
@@ -1817,14 +1807,14 @@
$$\begin{array}{c}
\termbdd{a_1}{\rho}{t_1}{b_1} \qquad \termbdd{a_2}{\rho}{t_2}{b_2}
\\ \hline
-\termbdd{a_1\cup a_2\cup \setass{t_1}}{\rho}{t_2}{{\footnotesize\t{simplify}}~b_1~b_2}
+\termbdd{a_1\cup a_2\cup \setass{t_1}}{\rho}{t_2}{{\t{\footnotesize simplify}}~b_1~b_2}
\end{array}$$
\noindent \rule\minipagewidth{0.1pt}
\begin{footnotesize}
The exception
-{\footnotesize\t{BddSimplifyError}} is raised if the varmaps in the hypotheses are not pointer equal
+{\t{\footnotesize BddSimplifyError}} is raised if the varmaps in the hypotheses are not pointer equal
\end{footnotesize}
\end{minipage}
\end{lrbox}
@@ -1832,7 +1822,7 @@
\vspace*{-2mm}
-\paragraph{Finding a satisfying assignment}\label{BddFindModel}{\(\)}\\
+\subsubsection*{Finding a satisfying assignment}\label{BddFindModel}
\vspace*{-1mm}
@@ -1852,7 +1842,7 @@
$$\begin{array}{c}
\termbdd{a}{\rho}{t}{b}
\\ \hline
-\termbdd{a\cup \setass{v_1=c_1,\ldots,v_p=c_p}}{\rho}{t}{{\footnotesize\t{TRUE}}}
+\termbdd{a\cup \setass{v_1=c_1,\ldots,v_p=c_p}}{\rho}{t}{{\t{\footnotesize TRUE}}}
\end{array}$$
\noindent \rule\minipagewidth{0.1pt}
@@ -1860,7 +1850,7 @@
\begin{footnotesize}
The set $\{v_1=c_1,\ldots,v_p=c_p\}$ is a satisfying assignment for $t$
($c_i$ is \T{} or \F{} for $1\leq i \leq p$). Exception
-{\footnotesize\t{BddFindModelError}} is raised if {\footnotesize\t{satone}}
+{\t{\footnotesize BddFindModelError}} is raised if {\t{\footnotesize satone}}
can't find a satisfying assignment.
\end{footnotesize}
\end{minipage}
@@ -2026,9 +2016,9 @@
\subsubsection{The structure \t{DerivedBddRules}}\label{DerivedBddRules}\index{HolBddLib!termbdd@... rules}
-This section notes a few of the more commonly used functions available in \texttt{DerivedBddRules}.
+This section notes a few of the more commonly used functions available in the structure \texttt{DerivedBddRules}.
-\paragraph{Varmaps}${}$\\
+\subsubsection*{Varmaps}
\bigskip
@@ -2047,7 +2037,7 @@
\end{lrbox}
\fbox{\usebox{\globalvarmap}}\index{HolBddLib!ML bindings!{global\_varmap}@\ml{global\_varmap}}
-\paragraph{Tests}${}$\\
+\subsubsection*{Tests}
\bigskip
@@ -2073,7 +2063,7 @@
\end{lrbox}
\fbox{\usebox{\isFALSE}}\index{HolBddLib!ML bindings!{isFALSE}@\ml{isFALSE}}
-\paragraph{Conversion to terms}${}$\\
+\subsubsection*{Conversion to terms}
\bigskip
@@ -2110,11 +2100,11 @@
\noindent \newsavebox\destBddOp
\begin{lrbox}\destBddOp
-\hbc{dest\_BddOp : term -> bddop * term * term}{Destruct a term corresponding to a BuDDY BDD binary operation (bddop). Fails with \texttt{dest\_BddOpError} if not such a term.}
+\hbc{dest\_BddOp : term -> bddop * term * term}{Destruct a term corresponding to a BuDDY BDD binary operation (bddop). Fails with\newline \texttt{dest\_BddOpError} if not such a term.}
\end{lrbox}
\fbox{\usebox{\destBddOp}}\index{HolBddLib!ML bindings!{dest\_BddOp}@\ml{dest\_BddOp}}
-\paragraph{Extracting theorems}${}$\\
+\subsubsection*{Extracting theorems}
\bigskip
@@ -2147,7 +2137,7 @@
\end{lrbox}
\fbox{\usebox{\findModel}}\index{HolBddLib!ML bindings!{findModel}@\ml{findModel}}
-\paragraph{Manipulating term\_bdd's}${}$\\
+\subsubsection*{Manipulating term\_bdd's}
\bigskip
@@ -2252,7 +2242,7 @@
\end{lrbox}
\fbox{\usebox{\BddSatone}}\index{HolBddLib!ML bindings!{BddSatone}@\ml{BddSatone}}
-\paragraph{Fixed points and traces}${}$\\
+\subsubsection*{Fixed points and traces}
\bigskip
Modified: HOL/Manual/Description/Makefile
===================================================================
--- HOL/Manual/Description/Makefile 2008-04-29 07:07:14 UTC (rev 5904)
+++ HOL/Manual/Description/Makefile 2008-04-29 09:00:05 UTC (rev 5905)
@@ -2,53 +2,63 @@
# Makefile for the hol DESCRIPTION
# =====================================================================
-# ---------------------------------------------------------------------
-# Pathnames: MAKEINDEX = makeindex script
-# ---------------------------------------------------------------------
+PDFLATEX=pdflatex
+DVILATEX=latex
MAKEINDEX=makeindex
BIBTEX=bibtex
+
CHAPTERS = conv.tex drules.tex libraries.tex misc.tex \
preface.tex semantics.tex syntax.tex \
tactics.tex theories.tex title.tex system.tex definitions.tex
+OTHER = ../LaTeX/commands.tex ../LaTeX/layout.sty ../LaTeX/ack.tex
-default: all
+default: pdf
+all: ps pdf
+ps: description.ps HolBdd.ps holCheck.ps
+pdf: description.pdf HolBdd.pdf holCheck.pdf
clean:
- rm -f *.dvi *.aux *.toc *.log *.idx *.ilg *.ind description.{ps,pdf} *.bbl *.blg HolBdd.{ps,pdf} holCheck.{ps,pdf}
+ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg *.ind description.{ps,pdf} \
+ *.bbl *.blg HolBdd.{ps,pdf} holCheck.{ps,pdf}
-description.dvi: description.tex $(CHAPTERS) ../LaTeX/commands.tex
-# (cd ../Logo ; make) # makes the lantern logo
- latex description.tex
- ${MAKEINDEX} description.idx
- ${BIBTEX} description
- latex description.tex
- latex description.tex
+description.pdf: description.tex $(CHAPTERS) $(OTHER)
+ ${PDFLATEX} description
+ ${MAKEINDEX} description
+ ${BIBTEX} description
+ ${PDFLATEX} description
+ ${PDFLATEX} description
+HolBdd.pdf: HolBdd.tex
+ ${PDFLATEX} HolBdd
+ ${BIBTEX} HolBdd
+ ${PDFLATEX} HolBdd
+ ${PDFLATEX} HolBdd
+
+holCheck.pdf: holCheck.tex
+ ${PDFLATEX} holCheck
+ ${PDFLATEX} holCheck
+
+description.dvi: description.tex $(CHAPTERS) $(OTHER)
+ ${DVILATEX} description
+ ${MAKEINDEX} description
+ ${BIBTEX} description
+ ${DVILATEX} description
+ ${DVILATEX} description
+
description.ps: description.dvi
dvips -Ppdf -G0 -f description.dvi > description.ps.tmp
mv description.ps.tmp $@
-description.pdf: description.ps
- ps2pdf description.ps
-
-HolBdd.ps:
- latex HolBdd.tex
- ${BIBTEX} HolBdd
- latex HolBdd.tex
- latex HolBdd.tex
+HolBdd.ps: HolBdd.tex
+ ${DVILATEX} HolBdd
+ ${BIBTEX} HolBdd
+ ${DVILATEX} HolBdd
+ ${DVILATEX} HolBdd
dvips -Ppdf -G0 -f HolBdd.dvi > HolBdd.ps.tmp
mv HolBdd.ps.tmp $@
-HolBdd.pdf: HolBdd.ps
- ps2pdf HolBdd.ps
-
-holCheck.ps:
- latex holCheck.tex
- latex holCheck.tex
+holCheck.ps: holCheck.tex
+ ${DVILATEX} holCheck
+ ${DVILATEX} holCheck
dvips -Ppdf -G0 -f holCheck.dvi > holCheck.ps.tmp
mv holCheck.ps.tmp $@
-
-holCheck.pdf: holCheck.ps
- ps2pdf holCheck.ps
-
-all: description.ps description.pdf HolBdd.pdf holCheck.pdf
Modified: HOL/Manual/Description/conv.tex
===================================================================
--- HOL/Manual/Description/conv.tex 2008-04-29 07:07:14 UTC (rev 5904)
+++ HOL/Manual/Description/conv.tex 2008-04-29 09:00:05 UTC (rev 5905)
@@ -202,12 +202,12 @@
conversions\index{conversions!operators on|(} are introduced. The
first one, infixed, is \ml{THENC}, which sequences conversions.
-\begin{boxed}
+\begin{holboxed}
\index{THENC@...}
\begin{verbatim}
op THENC : conv -> conv -> conv
\end{verbatim}
-\end{boxed}
+\end{holboxed}
\noindent If $c_1\ t_1$ evaluates to $\Gamma_1\ml{ |- }t_1\ml{=}t_2$ and
$c_2\ t_2$ evaluates to $\Gamma_2\ml{ |- }t_2\ml{=}t_3$, then
@@ -220,12 +220,12 @@
The second, also infixed, is \ml{ORELSEC}; this applies a second
conversion if the application of the first one fails.
-\begin{boxed}
+\begin{holboxed}
\index{ORELSEC@...}
\begin{verbatim}
op ORELSEC : conv -> conv -> conv
\end{verbatim}
-\end{boxed}
+\end{holboxed}
\noindent $\ml{(}c_1\ \ml{ORELSEC}\ c_2\ml{)}\ t$ evaluates to $c_1\ t$
if that evaluation succeeds, and to $c_2\ t$ otherwise. (The failure
@@ -236,12 +236,12 @@
successively\index{successive application!conversion operator for}
applies a conversion until it fails:
-\begin{boxed}
+\begin{holboxed}
\index{REPEATC@...}
\begin{verbatim}
REPEATC : conv -> conv
\end{verbatim}
-\end{boxed}
+\end{holboxed}
\noindent \ml{REPEATC}\ $c$ is intuitively equivalent to:
@@ -318,11 +318,11 @@
To produce, from a conversion $c$, a conversion that applies $c$ to every
subterm of a term, the function \ml{DEPTH\_CONV} can be applied to $c$:
-\begin{boxed}
+\begin{holboxed}
\index{DEPTH_CONV@...}
\begin{verbatim}
DEPTH_CONV : conv -> conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent \ml{DEPTH\_CONV}$\ c$ is a conversion
@@ -370,11 +370,11 @@
in characterizing the search strategy of {\tt TOP\_DEPTH\_CONV} should
study the \ML\ definitions near the end of this section.}
-\begin{boxed}
+\begin{holboxed}
\index{TOP_DEPTH_CONV@...}
\begin{verbatim}
TOP_DEPTH_CONV : conv -> conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent Thus:
@@ -385,11 +385,11 @@
Finally, the simpler function \ml{ONCE\_DEPTH\_CONV} is provided:
-\begin{boxed}
+\begin{holboxed}
\index{ONCE_DEPTH_CONV@...}
\begin{verbatim}
ONCE_DEPTH_CONV : conv -> conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent $\ml{ONCE\_DEPTH\_CONV}\ c\ t$ applies $c$ once to the first
term (and only the first term)
@@ -410,13 +410,13 @@
\ml{CONV\_RULE} or \ml{CONV\_TAC}, respectively.
-\begin{boxed}
+\begin{holboxed}
\index{CONV_RULE@...}
\index{CONV_TAC@...}
\begin{verbatim}
CONV_RULE : conv -> thm -> thm
CONV_TAC : conv -> tactic
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent $\ml{CONV\_RULE}\ c\ \ml{(|- }t\ml{)}$ returns $\ml{|- }t'$, where
$c\ t$ evaluates to the equation
@@ -433,11 +433,11 @@
For example, the built-in rule \ml{BETA\_RULE} reduces some
of the $\beta$-redex subterms of a term.
-\begin{boxed}
+\begin{holboxed}
\index{BETA_RULE@...}
\begin{verbatim}
BETA_RULE : thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent It is defined by:
@@ -496,11 +496,11 @@
\ml{ORELSEC}\index{ORELSEC@...}}, useful
in building functions.
-\begin{boxed}
+\begin{holboxed}
\index{NO_CONV@...}
\begin{verbatim}
NO_CONV : conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent $\ml{NO\_CONV}\ t$ always fails.
@@ -508,11 +508,11 @@
returns $c\ t$ for the first conversion $c$, in a list of conversions,
for which the evaluation of $c\ t$ succeeds.
-\begin{boxed}
+\begin{holboxed}
\index{FIRST_CONV@...}
\begin{verbatim}
FIRST_CONV : conv list -> conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent $\ml{FIRST\_CONV [}c_1\ml{;}\ldots\ml{;}c_n\ml{]}$ is equivalent,
intuitively, to:
@@ -533,22 +533,22 @@
The conversion \ml{ALL\_CONV} is an identity for \ml{THENC},\index{THENC@...}} useful
in building functions.
-\begin{boxed}
+\begin{holboxed}
\index{ALL_CONV@...}
\begin{verbatim}
ALL_CONV : conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent \ml{ALL\_CONV\ $t$} evaluates to \ml{|-\ $t$=$t$}. It is
defined as being identical to \ml{REFL}.\index{REFL@...}}
The function \ml{EVERY\_CONV} applies a list of conversions in sequence.
-\begin{boxed}
+\begin{holboxed}
\index{EVERY_CONV@...}
\begin{verbatim}
EVERY_CONV : conv list -> conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent $\ml{EVERY\_CONV [}c_1\ml{;}\ldots\ml{;}c_n\ml{]}$ is equivalent,
intuitively, to:
@@ -569,11 +569,11 @@
The operator \ml{CHANGED\_CONV} converts one conversion to another that
fails on arguments that it cannot change.
-\begin{boxed}
+\begin{holboxed}
\index{CHANGED_CONV@...}
\begin{verbatim}
CHANGED_CONV : conv -> conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent If $c\ t$ evaluates to $\ml{|-}\ t\ml{=}t'$, then
$\ml{CHANGED\_CONV}\ c\ t$ also evaluates to $\ml{|-}\ t\ml{=}t'$,
@@ -583,11 +583,11 @@
The operator \ml{TRY\_CONV} maps one conversion to another that
always succeeds, by replacing failures with the identity conversion.
-\begin{boxed}
+\begin{holboxed}
\index{TRY_CONV@...}
\begin{verbatim}
TRY_CONV : conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent If $c\ t$ evaluates to $\ml{|-}\ t\ml{=}t'$, then
$\ml{TRY\_CONV}\ c\ t$ also evaluates to $\ml{|-}\ t\ml{=}t'$. If
@@ -605,13 +605,13 @@
immediate subterms of a term. These use the \ML\ functions:
-\begin{boxed}
+\begin{holboxed}
\index{MK_COMB@...}
\index{MK_ABS@...}
\begin{verbatim}
MK_COMB : thm # thm -> thm
MK_ABS : thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent \ml{MK\_COMB} and \ml{MK\_ABS} implement the following derived rules:
@@ -626,11 +626,11 @@
applies a conversion to the immediate subterms
of a term.
-\begin{boxed}
+\begin{holboxed}
\index{SUB_CONV@...}
\begin{verbatim}
SUB_CONV : conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent In particular:
@@ -666,7 +666,7 @@
to the immediate subterms of a term, are as follows:
-\begin{boxed}
+\begin{holboxed}
\index{RATOR_CONV@...}
\index{RAND_CONV@...}
\index{ABS_CONV@...}
@@ -674,7 +674,7 @@
RATOR_CONV : conv -> conv
RAND_CONV : conv -> conv
ABS_CONV : conv -> conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent \ml{RATOR\_CONV}$\ c$ converts the operator of an application using
$c$; \ml{RAND\_CONV}$\ c$ converts the operand of an application; and
@@ -751,10 +751,10 @@
The conversion:
-\begin{boxed}\index{PAIRED_BETA_CONV@...}
+\begin{holboxed}\index{PAIRED_BETA_CONV@...}
\begin{verbatim}
PAIRED_BETA_CONV : conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent does
generalized beta-conversion of tupled lambda abstractions applied to
@@ -784,10 +784,10 @@
The conversion:
-\begin{boxed}\index{ADD_CONV@...}
+\begin{holboxed}\index{ADD_CONV@...}
\begin{verbatim}
ADD_CONV : conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent does addition by formal proof.
If $n$ and $m$ are numerals then
@@ -812,10 +812,10 @@
The next conversion decides the equality of natural number
constants.
-\begin{boxed}\index{num_EQ_CONV@...}
+\begin{holboxed}\index{num_EQ_CONV@...}
\begin{verbatim}
num_EQ_CONV : conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent If $n$ and $m$ are terms constructed from numeral constants
and the successor function \ml{SUC}, then:
@@ -834,13 +834,13 @@
There are two useful built-in conversions for lists:
-\begin{boxed}
+\begin{holboxed}
\index{LENGTH_CONV@...}
\index{list_EQ_CONV@...}
\begin{verbatim}
LENGTH_CONV : conv
list_EQ_CONV: conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\ml{LENGTH\_CONV}: computes the length of a list.
A call to:
@@ -887,10 +887,10 @@
A conversion for reducing {\tt let}-terms is now provided.
-\begin{boxed}\index{let_CONV@...}
+\begin{holboxed}\index{let_CONV@...}
\begin{verbatim}
let_CONV : conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent Given a term:
@@ -946,10 +946,10 @@
The conversion
-\begin{boxed}\index{X_SKOLEM_CONV@...}
+\begin{holboxed}\index{X_SKOLEM_CONV@...}
\begin{verbatim}
X_SKOLEM_CONV : term -> conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent takes a variable parameter, \ml{$f$} say, and
proves:
@@ -1121,11 +1121,11 @@
The rewriting primitive in \HOL\ is \ml{REWR\_CONV}:
-\begin{boxed}
+\begin{holboxed}
\index{REWR_CONV@...}
\begin{verbatim}
REWR_CONV : thm -> conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\noindent $\ml{REWR\_CONV (}\Gamma\ml{ |- }u \ml{=}v\ml{) }t$ evaluates to a
theorem $\Gamma\ml{ |- }t\ml{=}t'$
Modified: HOL/Manual/Description/definitions.tex
===================================================================
--- HOL/Manual/Description/definitions.tex 2008-04-29 07:07:14 UTC (rev 5904)
+++ HOL/Manual/Description/definitions.tex 2008-04-29 09:00:05 UTC (rev 5905)
@@ -555,8 +555,8 @@
\rewruse
\item[\texttt{\_fn\_updates}] The definitions of the functional update
functions.
-\item[\texttt{\_accfupds}] A theorem stating simpler forms for
- expressions of the form $\field{i}\, (\field{j}\update\;f\; r)$. If
+\item[\texttt{\_accfupds}] A theorem that states simpler forms for
+ expressions that are of the form $\field{i}\, (\field{j}\update\;f\; r)$. If
$i = j$, then the RHS is $f (\field{i}(r))$, if not, it is $(\field{i}\;r)$.
\rewruse
\item[\texttt{\_component\_equality}] A theorem stating that $(r_1 =
@@ -618,7 +618,7 @@
some details which are apparent at the lower level are no longer
visible at the higher level. The logic is simplified.
-However, simply forming a new type does not complete the quotient operation.
+Simply forming a new type does not complete the quotient operation.
Rather, one wishes to recreate the
%significant parts of the
pre-existing logical environment at the new,
@@ -887,7 +887,7 @@
and make the expression valid.
Note that the pattern \ml{0} is acceptable to either group.
-Patterns can also be nested, as shown in the next example, where
+Patterns can be nested as well, as shown in the next example, where
the function \ml{parents} returns a pair containing the person's father
and/or mother, where each is represented by \ml{NONE} if deceased.
%
@@ -1289,7 +1289,6 @@
\setcounter{sessioncount}{0}
\begin{session}
-\begin{hol}
\begin{verbatim}
val qsort_def =
Hol_defn "qsort"
@@ -1299,12 +1298,10 @@
++ [h] ++
qsort ord (FILTER (\x. ~(ord x h)) t))`
\end{verbatim}
-\end{hol}
\end{session}
which returns the following value of type \ml{defn}, but does not try
to prove termination.
\begin{session}
-\begin{hol}
\begin{verbatim}
HOL function definition (recursive)
@@ -1330,7 +1327,6 @@
1. !t h ord. R (ord,FILTER (\x. ord x h) t) (ord,h::t)
2. WF R
\end{verbatim}
-\end{hol}
\end{session}
The type \ml{defn} has a prettyprinter installed for it: the above
@@ -1340,7 +1336,6 @@
\ml{Defn.tgoal}, which sets up a termination proof in a goalstack.
%
\begin{session}
-\begin{hol}
\begin{verbatim}
Defn.tgoal qsort_def;
@@ -1352,7 +1347,6 @@
(!t h ord. R (ord,FILTER (\x. ~ord x h) t) (ord,h::t)) /\
(!t h ord. R (ord,FILTER (\x. ord x h) t) (ord,h::t)) /\ WF R
\end{verbatim}
-\end{hol}
\end{session}
%
The goal is to find a wellfounded relation on the arguments to \holtxt{qsort}
@@ -1364,7 +1358,6 @@
prove.
\begin{session}
-\begin{hol}
\begin{verbatim}
- e (WF_REL_TAC `measure (LENGTH o SND)`);
OK..
@@ -1374,7 +1367,6 @@
!t h ord. LENGTH (FILTER (\x. ~ord x h) t) < LENGTH (h::t)
\end{verbatim}
-\end{hol}
\end{session}
%
Execution of \ml{WF\_REL\_TAC} has automatically proved the
@@ -1390,7 +1382,6 @@
in the current theory segment before the recursion equations are returned:
\begin{session}
-\begin{hol}
\begin{verbatim}
- val qsort_def = tDefine "qsort"
`(qsort ord [] = []) /\
@@ -1405,14 +1396,12 @@
qsort ord (FILTER (\x. ord x h) t) ++ [h] ++
qsort ord (FILTER (\x. ~ord x h) t)) : thm
\end{verbatim}
-\end{hol}
\end{session}
The custom induction theorem for a function can be obtained by using \holtxt{fetch},
which returns named elements in the specified theory.\footnote{In a call to \texttt{fetch}, the
first argument denotes a theory; the current theory may be specified by \texttt{"-"}.}
\begin{session}
-\begin{hol}
\begin{verbatim}
- fetch "-" "qsort_ind";
> val qsort_ind =
@@ -1424,10 +1413,9 @@
==>
!v v1. P v v1 : thm
\end{verbatim}
-\end{hol}
\end{session}
-The induction theorem produced by \holtxt{Define} and \holtxt{tDefine} can
+\noindent The induction theorem produced by \holtxt{Define} and \holtxt{tDefine} can
be applied by \ml{recInduct}. See Section \ref{sec:bossLib} for details.
\subsubsection{Techniques for Proving Termination}
@@ -1450,7 +1438,6 @@
%
\setcounter{sessioncount}{0}
\begin{session}
-\begin{hol}
\begin{verbatim}
- val gcd_defn =
Hol_defn "gcd"
@@ -1465,7 +1452,6 @@
Initial goal:
?R. WF R /\ !v2 n. R (n MOD SUC v2,SUC v2) (SUC v2,n)
\end{verbatim}
-\end{hol}
\end{session}
%
The invocation \holtxt{gcd(m,n)} recurses in its first argument, and
@@ -1484,7 +1470,6 @@
Now we must pick out the argument position to measure and
invoke \ml{WF\_REL\_TAC}:
\begin{session}
-\begin{hol}
\begin{verbatim}
- e (WF_REL_TAC `measure FST`);
OK..
@@ -1492,7 +1477,6 @@
> val it =
!v2 n. n MOD SUC v2 < SUC v2
\end{verbatim}
-\end{hol}
\end{session}
%
This goal is easy to prove with a few simple arithmetic facts.
@@ -1506,7 +1490,6 @@
branch. At the end of execution the tree has been linearized.
\setcounter{sessioncount}{0}
\begin{session}
-\begin{hol}
\begin{verbatim}
- Hol_datatype
`btree = Leaf
@@ -1528,7 +1511,6 @@
(!bt. R bt (Brh Leaf bt)) /\
!bt bt2 bt1. R (Brh bt1 (Brh bt2 bt)) (Brh (Brh bt1 bt2) bt)
\end{verbatim}
-\end{hol}
\end{session}
%
Since the size of the tree is unchanged in the last clause in the
@@ -1537,19 +1519,16 @@
\holtxt{Unbal} decrease the total weight in every case. One such assignment is
%
\begin{session}
-\begin{hol}
\begin{verbatim}
Define
`(Weight (Leaf) = 0) /\
(Weight (Brh x y) = (2 * Weight x) + (Weight y) + 1)`
\end{verbatim}
-\end{hol}
\end{session}
%
Now we can invoke \ml{WF\_REL\_TAC}:
%
\begin{session}
-\begin{hol}
\begin{verbatim}
e (WF_REL_TAC `measure Weight`);
OK..
@@ -1561,7 +1540,6 @@
!bt bt2 bt1.
Weight (Brh bt1 (Brh bt2 bt)) < Weight (Brh (Brh bt1 bt2) bt)
\end{verbatim}
-\end{hol}
\end{session}
%
Both of these goals are quite easy to prove.
@@ -1585,7 +1563,6 @@
%
\setcounter{sessioncount}{0}
\begin{session}
-\begin{hol}
\begin{verbatim}
val match_defn =
Hol_defn "match"
@@ -1600,7 +1577,6 @@
- val Match = Define `Match pat str = match pat str pat str`;
\end{verbatim}
-\end{hol}
\end{session}
%
The first clause of the definition states that if $p$ becomes exhausted, then a match has
@@ -1652,7 +1628,6 @@
$n$ is the length of the second argument. These lengths are then
compared lexicographically with respect to less-than ($<$).
\begin{session}
-\begin{hol}
\begin{verbatim}
Defn.tgoal match_defn;
@@ -1668,7 +1643,6 @@
LENGTH (TL s) < LENGTH s \/
(LENGTH (TL s) = LENGTH s) /\ LENGTH (TL s) < LENGTH (b::ss)
\end{verbatim}
-\end{hol}
\end{session}
%
The first subgoal needs a case-split on \holtxt{s} before it is proved by
@@ -1780,12 +1754,10 @@
%
\setcounter{sessioncount}{0}
\begin{session}
-\begin{hol}
\begin{verbatim}
Define `(SIGMA f [] = 0) /\
(SIGMA f (h::t) = f h + SIGMA f t)`;
\end{verbatim}
-\end{hol}
\end{session}
%
We then use \holtxt{SIGMA} in the definition of a function for
@@ -1793,7 +1765,6 @@
(finitely) branching tree.
%
\begin{session}
-\begin{hol}
\begin{verbatim}
Hol_datatype `ltree = Node of 'a => ltree list`;
@@ -1801,7 +1772,6 @@
"ltree_sigma"
`ltree_sigma f (Node v tl) = f v + SIGMA (ltree_sigma f) tl`;
\end{verbatim}
-\end{hol}
\end{session}
%
In this definition, \holtxt{SIGMA} is applied to a partial application
@@ -1812,7 +1782,6 @@
the following unhappy situation results:
%
\begin{session}
-\begin{hol}
\begin{verbatim}
HOL function definition (recursive)
@@ -1827,7 +1796,6 @@
0. WF R
1. !tl v f a. R (f,a) (f,Node v tl) : defn
\end{verbatim}
-\end{hol}
\end{session}
%
The termination conditions for \holtxt{ltree\_sigma} seem to
@@ -1854,7 +1822,6 @@
proper subterm of \holtxt{Node v tl}.
%
\begin{session}
-\begin{hol}
\begin{verbatim}
val _ = DefnBase.add_cong SIGMA_CONG;
@@ -1872,7 +1839,6 @@
0. WF R
1. !v f tl a. MEM a tl ==> R (f,a) (f,Node v tl)
\end{verbatim}
-\end{hol}
\end{session}
\subsection{Recursion Schemas}
@@ -1910,7 +1876,6 @@
%
\setcounter{sessioncount}{0}
\begin{session}
-\begin{hol}
\begin{verbatim}
- TotalDefn.DefineSchema
`linRec (x:'a) = if d(x) then e(x) else f(linRec(g x))`;
@@ -1924,7 +1889,6 @@
[..]
|- linRec d e f g x = if d x then e x else f (linRec d e f g (g x))
\end{verbatim}
-\end{hol}
\end{session}
%
The hypotheses of the returned theorem hold the abstract termination
@@ -1932,12 +1896,10 @@
stored in the current theory segment.
%
\begin{session}
-\begin{hol}
\begin{verbatim}
hyp it;
> val it = [``!x. ~d x ==> R (g x) x``, ``WF R``] : term list
\end{verbatim}
-\end{hol}
\end{session}
%
These constraints are abstract, since they place termination requirements
@@ -1993,7 +1955,6 @@
for the relations, saved under the name \ml{<stem>\_cases}. A cases
theorem is of the form
%
-\begin{hol}
\begin{verbatim}
(!a0 .. an. R1 a0 .. an = <R1's first rule possibility> \/
<R1's second rule possibility> \/ ...)
@@ -2003,14 +1964,13 @@
/\
...
\end{verbatim}
-\end{hol}
%
and is used to decompose an element in the relation into the
possible ways of obtaining it by the rules.
\end{itemize}
\paragraph{Strong Induction Principles}
-So called ``strong'' versions of induction principles (where instances
+So called ``strong'' versions of induction principles (in which instances
of the relation being defined appear as extra hypotheses), can be
automatically proved with a call to the function
\[
@@ -2072,20 +2032,17 @@
%
\setcounter{sessioncount}{0}
\begin{session}
-\begin{hol}
\begin{verbatim}
Hol_reln
`EVEN 0 /\
(!n. ODD n ==> EVEN (n + 1)) /\
(!n. EVEN n ==> ODD (n + 1))`;
\end{verbatim}
-\end{hol}
\end{session}
%
The result is three theorems
%
\begin{session}
-\begin{hol}
\begin{verbatim}
> val it =
(|- EVEN 0 /\
@@ -2105,7 +2062,6 @@
(!a1. ODD a1 = ?n. (a1 = n + 1) /\ EVEN n)
) : thm * thm * thm
\end{verbatim}
-\end{hol}
\end{session}
%
The next example shows how to inductively define the reflexive and
@@ -2115,7 +2071,6 @@
characterisation, not \holtxt{RTC} itself.
%
\begin{session}
-\begin{hol}
\begin{verbatim}
- Hol_reln `(!x. RTC R x x) /\
(!x z. (?y. R x y /\ RTC R y z) ==> RTC R x z)`;
@@ -2133,7 +2088,6 @@
|- !R a0 a1. RTC R a0 a1 = (a1 = a0) \/ ?y. R a0 y /\ RTC R y a1
) : thm * thm * thm
\end{verbatim}
-\end{hol}
\end{session}
%
The \ml{Hol\_reln} function may be used to define multiple relations,
Modified: HOL/Manual/Description/description.tex
===================================================================
--- HOL/Manual/Description/description.tex 2008-04-29 07:07:14 UTC (rev 5904)
+++ HOL/Manual/Description/description.tex 2008-04-29 09:00:05 UTC (rev 5905)
@@ -2,20 +2,16 @@
% HOL Manual LaTeX Source: description
% =====================================================================
-\documentclass[12pt]{book}
-\usepackage{charter}
+\documentclass[12pt,fleqn]{book}
\usepackage{latexsym}
%\usepackage{amsmath}
\usepackage{amssymb}
%\usepackage{amsbsy}
%\usepackage{amsthm}
\usepackage{makeidx}
-\usepackage{fleqn}
\usepackage{alltt}
\usepackage{../LaTeX/layout}
\usepackage{graphicx}
-%\usepackage{pst-node}
-\usepackage{epsfig}
\usepackage{url}
% ---------------------------------------------------------------------
@@ -43,8 +39,8 @@
% prelims
% ---------------------------------------------------------------------
- \pagenumbering{roman} % roman page numbers for prelims
- \setcounter{page}{1} % start at page 1
+% \pagenumbering{roman} % roman page numbers for prelims
+% \setcounter{page}{1} % start at page 1
\include{title} % description title page
\include{preface} % preface to entire description
@@ -52,9 +48,9 @@
\tableofcontents % table of contents
- \cleardoublepage
- \pagenumbering{arabic} % arabic page numbers
- \setcounter{page}{1} % start at page 1
+% \cleardoublepage
+% \pagenumbering{arabic} % arabic page numbers
+% \setcounter{page}{1} % start at page 1
% ---------------------------------------------------------------------
% part 1: The HOL Logic
@@ -112,7 +108,8 @@
% ---------------------------------------------------------------------
-
+\small
+\emergencystretch=14pt
\printindex
\end{document}
Modified: HOL/Manual/Description/drules.tex
===================================================================
--- HOL/Manual/Description/drules.tex 2008-04-29 07:07:14 UTC (rev 5904)
+++ HOL/Manual/Description/drules.tex 2008-04-29 09:00:05 UTC (rev 5905)
@@ -455,11 +455,11 @@
\subsection{Adding an assumption}
\index{derived rules, in HOL logic@... rules, in \HOL{} logic!list and derivations of some|(}
-\begin{boxed}
+\begin{holboxed}
\index{ADD_ASSUM@...}
\begin{verbatim}
ADD_ASSUM : term -> thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -481,12 +481,12 @@
\subsection{Undischarging}
-\begin{boxed}
+\begin{holboxed}
\index{implication, in HOL logic@..., in \HOL\ logic!inference rules for}
\index{UNDISCH@...}
\begin{verbatim}
UNDISCH : thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -507,13 +507,13 @@
\subsection{Symmetry of equality}
-\begin{boxed}
+\begin{holboxed}
\index{SYM@...}
\index{symmetry of equality rule, in HOL logic@... of equality rule, in \HOL\ logic}
\index{equality, in HOL logic@..., in \HOL\ logic!symmetry rule for}
\begin{verbatim}
SYM : thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
@@ -534,13 +534,13 @@
\subsection{Transitivity of equality}
-\begin{boxed}
+\begin{holboxed}
\index{transitivity of equality rule, in HOL logic@... of equality rule, in \HOL\ logic}
\index{equality, in HOL logic@..., in \HOL\ logic!transitivity rule for}
\index{TRANS@...}
\begin{verbatim}
TRANS : thm -> thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -559,11 +559,11 @@
\subsection{Application of a term to a theorem}\index{function application, in HOL logic@... application, in \HOL\ logic!inference rules for}
-\begin{boxed}
+\begin{holboxed}
\index{AP_TERM@...}
\begin{verbatim}
AP_TERM : term -> thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -581,11 +581,11 @@
\subsection{Application of a theorem to a term}
-\begin{boxed}
+\begin{holboxed}
\index{AP_THM@...}
\begin{verbatim}
AP_THM : thm -> conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -604,12 +604,12 @@
\subsection{Modus Ponens for equality}
\label{avra_eq_mp}
-\begin{boxed}
+\begin{holboxed}
\index{EQ_MP@...}
\index{equality, in HOL logic@..., in \HOL\ logic!MP rule for@...} rule for}
\begin{verbatim}
EQ_MP : thm -> thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -630,11 +630,11 @@
\subsection{Implication from equality}
\index{equality, in HOL logic@..., in \HOL\ logic!other rules for|(}
\index{implication, in HOL logic@..., in \HOL\ logic!inference rules for}
-\begin{boxed}
+\begin{holboxed}
\index{EQ_IMP_RULE@...}
\begin{verbatim}
EQ_IMP_RULE : thm -> (thm # thm)
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -683,11 +683,11 @@
\subsection{Equality-with-\T\ elimination}
-\begin{boxed}
+\begin{holboxed}
\index{EQT_ELIM@...}
\begin{verbatim}
EQT_ELIM : thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -705,12 +705,12 @@
\subsection{Specialization ($\forall$-elimination)}
-\begin{boxed}
+\begin{holboxed}
\index{SPEC@...}
\index{specialization rule, in HOL logic@... rule, in \HOL\ logic}
\begin{verbatim}
SPEC : term -> thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\label{avra_spec}
@@ -749,11 +749,11 @@
\subsection{Equality-with-\T\ introduction}
-\begin{boxed}
+\begin{holboxed}
\index{EQT_INTRO@...}
\begin{verbatim}
EQT_INTRO : thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -782,12 +782,12 @@
\subsection{Generalization ($\forall$-introduction)}\index{universal quantifier, in HOL logic@... quantifier, in \HOL\ logic!inference rules for}
-\begin{boxed}
+\begin{holboxed}
\index{GEN@...}
\index{generalization rule, in HOL logic@... rule, in \HOL\ logic}
\begin{verbatim}
GEN : term -> thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\label{avra_gen}
@@ -822,9 +822,9 @@
\subsection{Simple $\alpha$-conversion}
-\begin{boxed}\begin{verbatim}
+\begin{holboxed}\begin{verbatim}
SIMPLE_ALPHA
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -865,11 +865,11 @@
\subsection{$\eta$-conversion}
-\begin{boxed}
+\begin{holboxed}
\index{ETA_CONV@...}
\begin{verbatim}
ETA_CONV : conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
$$\turn(\lquant{x'}t\ x') = t$$
@@ -893,12 +893,12 @@
\subsection{Extensionality}
\index{universal quantifier, in HOL logic@... quantifier, in \HOL\ logic!inference rules for}
-\begin{boxed}
+\begin{holboxed}
\index{EXT@...}
\index{extensionality rule, in HOL logic@... rule, in \HOL\ logic}
\begin{verbatim}
EXT : thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -926,12 +926,12 @@
\subsection{$\hilbert$-introduction}
-\begin{boxed}
+\begin{holboxed}
\index{choice operator, in HOL logic@... operator, in \HOL\ logic!inference rules for}
\index{SELECT_INTRO@...}
\begin{verbatim}
SELECT_INTRO : thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -952,12 +952,12 @@
\subsection{$\hilbert$-elimination}
-\begin{boxed}
+\begin{holboxed}
\index{choice operator, in HOL logic@... operator, in \HOL\ logic!inference rules for}
\index{SELECT_ELIM@...}
\begin{verbatim}
SELECT_ELIM : thm -> (term # thm) -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -985,11 +985,11 @@
\subsection{$\exists$-introduction}
\index{existential quantifier, in HOL logic@... quantifier, in \HOL\ logic!inference rules for|(}
-\begin{boxed}
+\begin{holboxed}
\index{EXISTS@...}
\begin{verbatim}
EXISTS : (term # term) -> thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -1028,11 +1028,11 @@
\subsection{$\exists$-elimination}
-\begin{boxed}
+\begin{holboxed}
\index{CHOOSE@...}
\begin{verbatim}
CHOOSE : (term # thm) -> thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -1072,11 +1072,11 @@
\subsection{Use of a definition}
-\begin{boxed}
+\begin{holboxed}
\index{RIGHT_BETA@...}
\begin{verbatim}
RIGHT_BETA : thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -1103,11 +1103,11 @@
\subsection{Use of a definition}
-\begin{boxed}
+\begin{holboxed}
\index{RIGHT_LIST_BETA@...}
\begin{verbatim}
RIGHT_LIST_BETA : thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -1139,12 +1139,12 @@
\label{avra_conj}
-\begin{boxed}
+\begin{holboxed}
\index{CONJ@...}
\index{conjunction, in HOL logic@..., in \HOL\ logic!inference rule for}
\begin{verbatim}
CONJ : thm -> thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -1177,12 +1177,12 @@
\subsection{$\wedge$-elimination}
-\begin{boxed}
+\begin{holboxed}
\index{CONJUNCT1@...}
\index{CONJUNCT2@...}
\begin{verbatim}
CONJUNCT1 : thm -> thm, CONJUNCT2 : thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -1217,11 +1217,11 @@
\subsection{Right $\vee$-introduction}\index{disjunction, in HOL logic@..., in \HOL\ logic!inference rule for|(}
-\begin{boxed}
+\begin{holboxed}
\index{DISJ1@...}
\begin{verbatim}
DISJ1 : thm -> conv
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -1251,11 +1251,11 @@
\subsection{Left $\vee$-introduction}
-\begin{boxed}
+\begin{holboxed}
\index{DISJ2@...}
\begin{verbatim}
DISJ2 : term -> thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -1283,11 +1283,11 @@
\subsection{$\vee$-elimination}
-\begin{boxed}
+\begin{holboxed}
\index{DISJ_CASES@...}
\begin{verbatim}
DISJ_CASES : thm -> thm -> thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
@@ -1322,12 +1322,12 @@
\subsection{Classical contradiction rule}
\index{F@... of inference for}
-\begin{boxed}
+\begin{holboxed}
\index{CCONTR@...}
\index{contradiction rule, in HOL logic@... rule, in \HOL\ logic}
\begin{verbatim}
CCONTR : term -> thm -> thm
-\end{verbatim}\end{boxed}
+\end{verbatim}\end{holboxed}
\vspace{12pt plus2pt minus1pt}
Added: HOL/Manual/Description/figs/asr.pdf
===================================================================
(Binary files differ)
Property changes on: HOL/Manual/Description/figs/asr.pdf
___________________________________________________________________
Name: svn:mime-type
+ application/octet-stream
Added: HOL/Manual/Description/figs/bits.pdf
===================================================================
(Binary files differ)
Property changes on: HOL/Manual/Description/figs/bits.pdf
___________________________________________________________________
Name: svn:mime-type
+ application/octet-stream
Added: HOL/Manual/Description/figs/concat.pdf
===================================================================
(Binary files differ)
Property changes on: HOL/Manual/Description/figs/concat.pdf
___________________________________________________________________
Name: svn:mime-type
+ application/octet-stream
Added: HOL/Manual/Description/figs/ex.pdf
===================================================================
(Binary files differ)
Property changes on: HOL/Manual/Description/figs/ex.pdf
___________________________________________________________________
Name: svn:mime-type
+ application/octet-stream
Added: HOL/Manual/Description/figs/lsl.pdf
===================================================================
(Binary files differ)
Property changes on: HOL/Manual/Description/figs/lsl.pdf
___________________________________________________________________
Name: svn:mime-type
+ application/octet-stream
Added: HOL/Manual/Description/figs/lsr.pdf
===================================================================
(Binary files differ)
Property changes on: HOL/Manual/Description/figs/lsr.pdf
___________________________________________________________________
Name: svn:mime-type
+ application/octet-stream
Added: HOL/Manual/Description/figs/reverse.pdf
===================================================================
(Binary files differ)
Property changes on: HOL/Manual/Description/figs/reverse.pdf
___________________________________________________________________
Name: svn:mime-type
+ application/octet-stream
Added: HOL/Manual/Description/figs/ror.pdf
===================================================================
(Binary files differ)
Property changes on: HOL/Manual/Description/figs/ror.pdf
___________________________________________________________________
Name: svn:mime-type
+ application/octet-stream
Added: HOL/Manual/Description/figs/rrx.pdf
===================================================================
--- HOL/Manual/Description/figs/rrx.pdf (rev 0)
+++ HOL/Manual/Description/figs/rrx.pdf 2008-04-29 09:00:05 UTC (rev 5905)
@@ -0,0 +1,135 @@
+%PDF-1.3
+%\xC4\xE5\xF2\xE5\xEB\xA7\xF3\xA0\xD0\xC4\xC6
+4 0 obj
+<< /Length 5 0 R /Filter /FlateDecode >>
+stream
+x>\x8D\x9BI\xCE \xC7F\xF7}\x8A\xBE\x80\xDB5k- hgh\xE1\x96eC6 s\xE1\xEB\xFB\xBD/2\xAB\xEB\x97HJ"lv~\x95Cd\xCCU\xFC\xE5\xF9\xD7\xE7/\xCF\xE1\xB5
+\xF9\xEF\xF9\xCF矿\xFB<>?}~\x8E\xF9\xF3\xF9\xD3s>\x9F\xDB\xF0\xDA\xD7\xE74\x82\xED\xAF\xF5\xF9߿?d\xCD\xDA\xD6\xFC\x8F\x99\xDF?\xC6\xE7\xBFj\xEDw?<\x87\xFC\xF9\xE1;\xB6 \xF3\xF3O\xE3\xF3O\xF3\xCA\xD2q9\xF9\xFFO\xFF~\xEE \xEF\xE3k\xFA\xB8\xEFϿ>\x86\xD7r.\xE3x\xB0\xCBkۏe \xFDu\xAC\xC3y \xC3\x8A\xFE\xFCH\xFC\xC7\xE7\xE7|\xBCN\xFFk\xF4\x8D\xE7\xF6Z\xCF\xE9M#4\xF9\xA7VLYq>\xD9\xEC\xE3E~\x87\xC6q\x9A\xAEn\x85P\xF3)\\xE7\xD72 \xCFS\xF6\xFD\x8A\xBCǏ\x90\xF6?\xB8\xF3=\xFF\xFB\xD7\xEFl +\xB9\xF4\xEC\xBEL\xEE\x96 \xEBk\x9B\x8Em\x8E\xE3¯u~\x86\xCD :\x9E\xC7!
+?\x87\xFCuzm\xEB>\x9D\xCFI\xAE\xCB\xC8D\xB0y\x9E\x97'R:\xA6\xE9\ ??\x97\xFDuN\xF39?\xE7\x99 \xDBr\xB0\xFC''\xFEf\xF1\x8F_\xA1JAs\xF0\xE8a\x8FqRe\x96\x8DÎ\xFDux\xD88\xCEHx \xD9\xF8\x80S9l ѓ}\x96֟\xAE\xC5\xCF\xDB\xE2 \xAA\xEC\xD7\xF4j:\xA6\xD74
+ \x980\xA1g\x8Aq\xE7\xC1\x84"\xF2\xBF\xF9\xD1x\xB0@... w\xC3\xB7\xE1a\xF3\xA8\xEDy\xE7e}\xC1 ty:_\xC3tjL\xCB̺c=4\xDDmX7Mw>_\xF3\xB9\xCC\xD3s\x9E0\xFBc*\xD3\xFD\xC2b\xFCxs@...
+n8gj\x84\xCB>\xA8\xEE\xBB\xEE\xC4CU\xDF\xE3\\xE8å\xF3\x8BC\xC7q\x93\xB1;&\xDCV\xC7\xFE\xDB\xEA\x92\xDE\xF7ѩ/+\xF2\xB7b\xC7c\xE2\xF4a\x9F/^M0k]\xFCll\xFB \xE0\xCE9*\xAC\xE55,\xFC\x98\xF6Ym \x8C\xF0\xF3\x9Cf|\xDBp\x8C\x8F\x91\x99\xCBz`\xC3\xF0\x82n\x88 &\xBC\xFB\xB1?\xB7\xD2S\xA7/Xز\xEF\x98&l'\xB3\xF0\x8D\xEB\xB0Θ\xF4H \x9B\x87\xF1\xB1.Hf9D\xD6\xD7N\x9Cc\xDDW\xB5T\x9C\xA6\xD7y@...
+>\x90\xE5\xB2 \x9C\xF8\xF3f 뾝\xCAr\xDCd \xBF\xF0\x85\xD5D\x98\xEB\xF1\x82HNU\x98\xE8l|?>\xDFS! vBN<ȩ\xD8\xEE\xE5̡\xBFY\xFC\xF8w\xEE\xF8\xAB\\xA0|ŕS\xBC\xB3\x8B\xF7\xAF\xDF\xF5!* \x96\x89\xEAw\xBAQ\x8Cz=\xCCj \xFCGvP%\x8F\xDF\xFB~\xE1W\xF3\x89\xFF\xE3
+_\xD7>\xF39\x90輩\xCAb\xE3\xCE^\xF0w\xB6\xD5h4\xE5x\x8CM\x8D0iD\xD7\xE4y_m\xCC\xE8\xAB\x8F\xE7\xFA\xC2\xF1 ^\xA7\xA7\x8E\xD3H0\xACS\xC16N}h,Ǚx7OO%\xF9A%Х\x9C\xFA\x85\xD5^:Q\xDD\xC1ilk\xE5Q\xAF
+M| \xAFm\xC15캬\xBF=\xFFs\xE3\xD9\xDD_>\xAF:\xEEq&Ex\xEEx\xE2z\xB8P@... ^I\x8B\xE3Y\x86\xC3<
+36Ѐ\xE9u\xEC\xC7 |\xBE\xEEǃ\xB3\x8Fag\x8A\xC8v\xAC\xA7\xD4l\xE8\xB9'vz\xB0e>9\xABѐYc\xB6\xEEȃ8\xB3g'ׅRfa\x95c\x82);\xCDl\xBE \xDA?\xE2<q
|