--- a/doc-src/Ref/introduction.tex Tue May 04 10:26:00 1999 +0200
+++ b/doc-src/Ref/introduction.tex Tue May 04 11:27:25 1999 +0200
@@ -44,6 +44,8 @@
isabellehome \rangle\)/bin/isabelle}, though! See \texttt{isatool
install} in \emph{The Isabelle System Manual} of how to do this properly.}
+\medskip
+
The object-logic image to load may be also specified explicitly as an argument
to the {\tt isabelle} command, e.g.
\begin{ttbox}
@@ -76,7 +78,7 @@
\medskip Saving the {\ML} state is not enough. Record, on a file, the
top-level commands that generate your theories and proofs. Such a record
allows you to replay the proofs whenever required, for instance after making
-minor changes to the axioms. Ideally, your these sources will be somewhat
+minor changes to the axioms. Ideally, these sources will be somewhat
intelligible to others as a formal description of your work.
It is good practice to put all source files that constitute a separate
@@ -84,7 +86,7 @@
called \texttt{ROOT.ML} that contains appropriate commands to load all other
files required. Running \texttt{isabelle} with option \texttt{-u}
automatically loads \texttt{ROOT.ML} on entering the session. The
-\texttt{isatool usedir} utility provides some more options to manage your
+\texttt{isatool usedir} utility provides some more options to manage Isabelle
sessions, such as automatic generation of theory browsing information.
\medskip More details about the \texttt{isabelle} and \texttt{isatool}
@@ -145,7 +147,8 @@
commands may contain path variables (e.g.\ \texttt{\$ISABELLE_HOME}) that are
expanded appropriately. Note that \texttt{\~\relax} abbreviates
\texttt{\$HOME}, and \texttt{\~\relax\~\relax} abbreviates
-\texttt{\$ISABELLE_HOME}\index{*\$ISABELLE_HOME}.
+\texttt{\$ISABELLE_HOME}\index{*\$ISABELLE_HOME}. The syntax for path
+specifications follows Unix conventions.
\section{Reading theories}\label{sec:intro-theories}
@@ -181,10 +184,11 @@
the internal database of loaded theories, raising an error if absent.
\item[\ttindexbold{use_thy} "$name$";] reads theory $name$ from the file
- system, looking for $name$\texttt{.thy} and (optionally) $name$\texttt{.ML};
- also makes sure that all parent theories are loaded as well. In case some
- older versions have already been present, \texttt{use_thy} only tries to
- reload $name$ itself, but is content with any version of its parents.
+ system, looking for $name$\texttt{.thy} and $name$\texttt{.ML} (the latter
+ being optional). It also ensures that all parent theories are loaded as
+ well. In case some older versions have already been present,
+ \texttt{use_thy} only tries to reload $name$ itself, but is content with any
+ version of its ancestors.
\item[\ttindexbold{time_use_thy} "$name$";] same as \texttt{use_thy}, but
reports the time taken to process the actual theory parts and {\ML} files
@@ -221,11 +225,10 @@
(\S\ref{sec:goals-printing}).
\begin{ttdescription}
-\item[\ttindexbold{Pretty.setdepth} \(d\);]
- tells Isabelle's pretty printer to limit the printing depth to~$d$. This
- affects Isabelle's display of theorems and terms. The default value
- is~0, which permits printing to an arbitrary depth. Useful values for
- $d$ are~10 and~20.
+\item[\ttindexbold{Pretty.setdepth} \(d\);] tells Isabelle's pretty printer to
+ limit the printing depth to~$d$. This affects the display of theorems and
+ terms. The default value is~0, which permits printing to an arbitrary
+ depth. Useful values for $d$ are~10 and~20.
\item[\ttindexbold{Pretty.setmargin} \(m\);]
tells Isabelle's pretty printer to assume a right margin (page width)
--- a/doc-src/Ref/ref.ind Tue May 04 10:26:00 1999 +0200
+++ b/doc-src/Ref/ref.ind Tue May 04 11:27:25 1999 +0200
@@ -27,7 +27,7 @@
\item {\tt abstract_over}, \bold{63}
\item {\tt abstract_rule}, \bold{49}
\item {\tt aconv}, \bold{63}
- \item {\tt add_path}, \bold{59}
+ \item {\tt add_path}, \bold{60}
\item {\tt addaltern}, \bold{137}
\item {\tt addbefore}, \bold{137}
\item {\tt Addcongs}, \bold{107}
@@ -189,7 +189,7 @@
\item {\tt cprems_of}, \bold{45}
\item {\tt cprop_of}, \bold{44}
\item {\tt CPure} theory, 55
- \item {\tt CPure.thy}, \bold{60}
+ \item {\tt CPure.thy}, \bold{61}
\item {\tt crep_thm}, \bold{45}
\item {\tt cterm} ML type, 64
\item {\tt cterm_instantiate}, \bold{43}
@@ -423,7 +423,6 @@
\item {\tt match_tac}, \bold{21}, 134
\item {\tt max_pri}, 70, \bold{76}
\item {\tt merge_ss}, \bold{109}
- \item {\tt merge_theories}, \bold{61}
\item meta-assumptions, 37, 46, 48, 51
\subitem printing of, 5
\item meta-equality, 47--49
@@ -434,10 +433,10 @@
\subitem in theorems, 43
\item meta-rules, \see{meta-rules}{1}, 46--52
\item {\tt METAHYPS}, 19, \bold{37}
- \item mixfix declarations, 56, 75--80
+ \item mixfix declarations, 57, 75--80
\item {\tt mk_atomize}, \bold{127}
\item {\tt mk_simproc}, \bold{123}
- \item {\tt ML} section, 57, 97, 99
+ \item {\tt ML} section, 58, 97, 99
\item model checkers, 81
\item {\tt mp} theorem, \bold{143}
\item {\tt mp_tac}, \bold{142}
@@ -529,7 +528,7 @@
\item {\tt PROP} symbol, 71
\item {\textit {prop}} type, 65, 72
\item {\tt prop} nonterminal, \bold{70}, 82
- \item {\tt ProtoPure.thy}, \bold{60}
+ \item {\tt ProtoPure.thy}, \bold{61}
\item {\tt prove_goal}, 14, \bold{16}
\item {\tt prove_goalw}, \bold{16}
\item {\tt prove_goalw_cterm}, \bold{16}
@@ -540,7 +539,7 @@
\item {\tt pttrn} nonterminal, \bold{72}
\item {\tt pttrns} nonterminal, \bold{72}
\item {\tt Pure} theory, 55, 70, 74
- \item {\tt Pure.thy}, \bold{60}
+ \item {\tt Pure.thy}, \bold{61}
\item {\tt push_proof}, \bold{17}
\item {\tt pwd}, \bold{3}
@@ -636,14 +635,14 @@
\item {\tt settermless}, \bold{121}
\item {\tt setup}
\subitem simplifier, 129
- \subitem theory, 57
+ \subitem theory, 58
\item shortcuts
\subitem for \texttt{by} commands, 14
\subitem for tactics, 23
\item {\tt show_brackets}, \bold{5}
\item {\tt show_consts}, \bold{6}
\item {\tt show_hyps}, \bold{5}
- \item {\tt show_path}, \bold{59}
+ \item {\tt show_path}, \bold{60}
\item {\tt show_sorts}, \bold{5}, 89, 97
\item {\tt show_tags}, \bold{5}
\item {\tt show_types}, \bold{5}, 89, 92, 99
@@ -795,7 +794,6 @@
\subitem taking apart, 44
\item theories, 55--68
\subitem axioms of, 11
- \subitem constructing, \bold{60}
\subitem inspecting, \bold{61}
\subitem parent, \bold{55}
\subitem reading, 3, 59
@@ -838,7 +836,7 @@
\subitem of tactics, 30
\subitem of unification, 46
\item {\tt transfer}, \bold{60}
- \item {\tt transfer_sg}, \bold{60}
+ \item {\tt transfer_sg}, \bold{61}
\item {\tt transitive}, \bold{49}
\item translations, 96--99
\subitem parse, 80, 88
--- a/doc-src/Ref/ref.tex Tue May 04 10:26:00 1999 +0200
+++ b/doc-src/Ref/ref.tex Tue May 04 11:27:25 1999 +0200
@@ -1,5 +1,5 @@
\documentclass[12pt]{report}
-\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../pdfsetup}
+\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,pdfsetup}
%% $Id$
%\includeonly{introduction}
@@ -7,7 +7,7 @@
%%% to delete old ones: \\indexbold{\*[^}]*}
%% run sedindex ref to prepare index file
%%% needs chapter on Provers/typedsimp.ML?
-\title{\includegraphics[scale=0.5]{isabelle.eps} \\[4ex] The Isabelle Reference Manual}
+\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle Reference Manual}
\author{{\em Lawrence C. Paulson}\\
Computer Laboratory \\ University of Cambridge \\
--- a/doc-src/Ref/theories.tex Tue May 04 10:26:00 1999 +0200
+++ b/doc-src/Ref/theories.tex Tue May 04 11:27:25 1999 +0200
@@ -27,11 +27,11 @@
\section{Defining theories}\label{sec:ref-defining-theories}
-Theories are usually defined using theory definition files (which have a name
-suffix {\tt .thy}). There is also a low level interface provided by certain
-\ML{} functions (see \S\ref{BuildingATheory}).
-Appendix~\ref{app:TheorySyntax} presents the concrete syntax for theory
-definitions; here is an explanation of the constituent parts:
+Theories are defined via theory files $name$\texttt{.thy} (there are also
+\ML-level interfaces which are only intended for people building advanced
+theory definition packages). Appendix~\ref{app:TheorySyntax} presents the
+concrete syntax for theory files; here follows an explanation of the
+constituent parts.
\begin{description}
\item[{\it theoryDef}] is the full definition. The new theory is called $id$.
It is the union of the named {\bf parent
@@ -39,6 +39,15 @@
components. \thydx{Pure} and \thydx{CPure} are the basic theories, which
contain only the meta-logic. They differ just in their concrete syntax for
function applications.
+
+ The new theory begins as a merge of its parents.
+ \begin{ttbox}
+ Attempt to merge different versions of theories: "\(T@1\)", \(\ldots\), "\(T@n\)"
+ \end{ttbox}
+ This error may especially occur when a theory is redeclared --- say to
+ change an inappropriate definition --- and bindings to old versions persist.
+ Isabelle ensures that old and new theories of the same name are not involved
+ in a proof.
\item[$classes$]
is a series of class declarations. Declaring {\tt$id$ < $id@1$ \dots\
@@ -250,7 +259,8 @@
\item[\ttindexbold{update_thy} "$name$";] is similar to \texttt{use_thy}, but
ensures that theory $name$ is fully up-to-date with respect to the file
- system --- apart from $name$ itself its parents may be reloaded as well.
+ system --- apart from $name$ itself any of its ancestors may be reloaded as
+ well.
\item[\ttindexbold{touch_thy} "$name$";] marks theory node $name$ of the
internal graph as outdated. While the theory remains usable, subsequent
@@ -261,7 +271,7 @@
afterwards. Resetting the \texttt{delete_tmpfiles} flag inhibits this,
leaving the generated code for debugging purposes. The basic location for
temporary files is determined by the \texttt{ISABELLE_TMP} environment
- variable, which is private to the running Isabelle process (it may be
+ variable (which is private to the running Isabelle process and may be
retrieved by \ttindex{getenv} from {\ML}).
\end{ttdescription}
@@ -279,7 +289,7 @@
\begin{ttdescription}
\item[\ttindexbold{show_path}();] displays the load path components in
- canonical string representation, which is always according to Unix rules.
+ canonical string representation (which is always according to Unix rules).
\item[\ttindexbold{add_path} "$dir$";] adds component $dir$ to the beginning
of the load path.
@@ -291,11 +301,11 @@
(current directory) only.
\end{ttdescription}
-In operations referring indirectly to some file, such as
-\texttt{use_thy~"$name$"}, the argument may be prefixed by some directory that
-will be used as temporary load path. Note that, depending on which parts of
-the ancestry of $name$ are already loaded, the dynamic change of paths might
-be hard to predict. Use this feature with care only.
+In operations referring indirectly to some file, the argument may be prefixed
+by a directory that will be used as temporary load path, e.g.\
+\texttt{use_thy~"$dir/name$"}. Note that, depending on which parts of the
+ancestry of $name$ are already loaded, the dynamic change of paths might be
+hard to predict. Use this feature with care only.
\section{Basic operations on theories}\label{BasicOperationsOnTheories}
@@ -334,14 +344,11 @@
\end{ttdescription}
-\subsection{*Building a theory}
-\label{BuildingATheory}
-\index{theories!constructing|bold}
+\subsection{*Primitive theories}
\begin{ttbox}
ProtoPure.thy : theory
Pure.thy : theory
CPure.thy : theory
-merge_theories : string -> theory * theory -> theory
\end{ttbox}
\begin{description}
\item[\ttindexbold{ProtoPure.thy}, \ttindexbold{Pure.thy},
@@ -352,20 +359,14 @@
$t(u@1, \ldots, u@n)$ in \texttt{Pure} vs.\ $t\,u@1,\ldots\,u@n$ in
\texttt{CPure}. \texttt{ProtoPure} is their common parent,
containing no syntax for printing prefix applications at all!
-
-\item[\ttindexbold{merge_theories} $name$ ($thy@1$, $thy@2$)] merges
- the two theories $thy@1$ and $thy@2$, creating a new named theory
- node. The resulting theory contains all of the syntax, signature
- and axioms of the constituent theories. Merging theories that
- contain different identification stamps of the same name fails with
- the following message
-\begin{ttbox}
-Attempt to merge different versions of theories: "\(T@1\)", \(\ldots\), "\(T@n\)"
-\end{ttbox}
-This error may especially occur when a theory is redeclared --- say to
-change an inappropriate definition --- and bindings to old versions
-persist. Isabelle ensures that old and new theories of the same name
-are not involved in a proof.
+
+%%FIXME
+%\item[\ttindexbold{merge_theories} $name$ ($thy@1$, $thy@2$)] merges
+% the two theories $thy@1$ and $thy@2$, creating a new named theory
+% node. The resulting theory contains all of the syntax, signature
+% and axioms of the constituent theories. Merging theories that
+% contain different identification stamps of the same name fails with
+% the following message
%% FIXME
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends