--- a/ANNOUNCE Thu Mar 07 22:52:07 2002 +0100
+++ b/ANNOUNCE Thu Mar 07 23:21:19 2002 +0100
@@ -18,7 +18,7 @@
Isabelle2002 is the official version to go along with that book
(by Tobias Nipkow, Larry Paulson, Markus Wenzel).
- * Pure: explicit proof terms for all internal inferences:
+ * Pure: explicit proof terms for all internal inferences;
object-logics, proof tools etc. will benefit automatically
(by Stefan Berghofer).
@@ -27,28 +27,30 @@
operations, and type-inference for structured specifications
(by Markus Wenzel).
- * Pure/Isar: streamlined induction proof patterns
+ * Pure/Isar: streamlined cases/induction proof patterns
(by Markus Wenzel).
* Pure/HOL: infrastructure for generating functional and relational
- code, using the ML run-time environment (by Stefan Berghofer).
+ code, using the ML run-time environment
+ (by Stefan Berghofer).
- * HOL/library: numerals on all number types; several
- improvements of tuple and record types; new definite description
- operator; keep Hilbert's epsilon (Axiom of Choice) out of basic theories.
+ * HOL/library: numerals on all number types; several improvements of
+ tuple and record types; new definite description operator; keep
+ Hilbert's epsilon (Axiom of Choice) out of basic theories
+ (by Stefan Berghofer, Larry Paulson, Markus Wenzel).
* HOL/Bali: large application concerning formal treatment of Java.
(by David von Oheimb and Norbert Schirmer).
* HOL/HoareParallel: large application concerning verification of
parallel imperative programs (Owicki-Gries method, Rely-Guarantee
- method, examples of garbage collection, mutual exclusion, etc.)
+ method, examples of garbage collection, mutual exclusion)
(by Leonor Prensa Nieto).
* HOL/GroupTheory: group theory examples including Sylow's theorem
- (by Florian Kammüller).
+ (by Florian Kammueller).
- * HOL/IMP: new proofs in Isar format
+ * HOL/IMP: several new proofs in Isar format
(by Gerwin Klein).
* HOL/MicroJava: exception handling on the bytecode level
@@ -61,10 +63,8 @@
(by Markus Wenzel).
* System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting
- larger heap size of applications.
-
- * System: support for MacOS X (for Poly/ML and SML/NJ).
-
+ larger heap size of applications; support for MacOS X (Poly/ML and
+ SML/NJ).
You may get Isabelle2002 from any of the following mirror sites:
--- a/NEWS Thu Mar 07 22:52:07 2002 +0100
+++ b/NEWS Thu Mar 07 23:21:19 2002 +0100
@@ -210,7 +210,7 @@
- remove all special provisions on numerals in proofs;
-* HOL: simp rules nat_number_of expand numerals on nat to Suc/0
+* HOL: simp rules nat_number expand numerals on nat to Suc/0
representation (depends on bin_arith_simps in the default context);
* HOL: symbolic syntax for x^2 (numeral 2);
--- a/doc-src/IsarRef/conversion.tex Thu Mar 07 22:52:07 2002 +0100
+++ b/doc-src/IsarRef/conversion.tex Thu Mar 07 23:21:19 2002 +0100
@@ -188,7 +188,7 @@
This may be replaced by using the $unfold$ proof method explicitly.
\begin{matharray}{l}
\LEMMA{name}{\texttt"{\phi}\texttt"} \\
-\quad \APPLY{unfold~def@1~\dots} \\
+\quad \APPLY{(unfold~def@1~\dots)} \\
\end{matharray}
@@ -224,7 +224,7 @@
$simp$, $blast$, or $auto$. This could work as follows:
\begin{matharray}{l}
\LEMMA{}{\texttt"{\phi@1 \Imp \dots \Imp \psi}\texttt"} \\
- \quad \BYY{unfold~defs}{blast} \\
+ \quad \BYY{(unfold~defs)}{blast} \\
\end{matharray}
Note that classic Isabelle would support this form only in the special case
where $\phi@1$, \dots are atomic statements (when using the standard
@@ -265,7 +265,7 @@
\begin{matharray}{l}
\LEMMA{name}{\texttt"{\All{\vec x}\vec\phi \Imp \psi}\texttt"} \\
- \quad \APPLY{atomize~(full)} \\
+ \quad \APPLY{(atomize~(full))} \\
\quad \APPLY{meth@1} \\
\qquad \vdots \\
\quad \DONE \\
--- a/doc-src/IsarRef/generic.tex Thu Mar 07 22:52:07 2002 +0100
+++ b/doc-src/IsarRef/generic.tex Thu Mar 07 23:21:19 2002 +0100
@@ -230,8 +230,8 @@
\quad \PROOF{succeed} \\
\qquad \FIX{thesis} \\
\qquad \ASSUME{that~[intro?]}{\All{\vec x} \vec\phi \Imp thesis} \\
- \qquad \SHOW{}{thesis} \\
- \quad\qquad \APPLY{insert~that} \\
+ \qquad \THUS{}{thesis} \\
+ \quad\qquad \APPLY{-} \\
\quad\qquad \USING{\vec b}~~\langle proof\rangle \\
\quad \QED{} \\
\quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\
--- a/doc-src/IsarRef/logics.tex Thu Mar 07 22:52:07 2002 +0100
+++ b/doc-src/IsarRef/logics.tex Thu Mar 07 23:21:19 2002 +0100
@@ -228,18 +228,16 @@
\medskip
In Isabelle/HOL record types have to be defined explicitly, fixing their field
-names and types, and their (optional) parent record (see
-{\S}\ref{sec:hol-record-def}). Afterwards, records may be formed using above
-syntax, while obeying the canonical order of fields as given by their
-declaration. The record package provides several standard operations like
-selectors and updates (see {\S}\ref{sec:hol-record-ops}). The common setup
-for various generic proof tools enable succinct reasoning patterns (see
-{\S}\ref{sec:hol-record-thms}). See also the Isabelle/HOL tutorial
-\cite{isabelle-hol-book} for further instructions on using records in
+names and types, and their (optional) parent record. Afterwards, records may
+be formed using above syntax, while obeying the canonical order of fields as
+given by their declaration. The record package provides several standard
+operations like selectors and updates. The common setup for various generic
+proof tools enable succinct reasoning patterns. See also the Isabelle/HOL
+tutorial \cite{isabelle-hol-book} for further instructions on using records in
practice.
-\subsubsection{Record specifications}\label{sec:hol-record-def}
+\subsubsection{Record specifications}
\indexisarcmdof{HOL}{record}
\begin{matharray}{rcl}
@@ -275,7 +273,7 @@
\end{descr}
-\subsubsection{Record operations}\label{sec:hol-record-ops}
+\subsubsection{Record operations}
Any record definition of the form presented above produces certain standard
operations. Selectors and updates are provided for any field, including the
@@ -343,7 +341,7 @@
\noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ actually coincide for root records.
-\subsubsection{Derived rules and proof tools}\label{sec:hol-record-thms}
+\subsubsection{Derived rules and proof tools}
The record package proves several results internally, declaring these facts to
appropriate proof tools. This enables users to reason about record structures
@@ -425,9 +423,8 @@
old-style theory syntax being used there! Apart from proper proof methods for
case-analysis and induction, there are also emulations of ML tactics
\texttt{case_tac} and \texttt{induct_tac} available, see
-\S\ref{sec:hol-induct-tac} or \S\ref{sec:zf-induct-tac}; these admit to refer
-directly to the internal structure of subgoals (including internally bound
-parameters).
+\S\ref{sec:hol-induct-tac}; these admit to refer directly to the internal
+structure of subgoals (including internally bound parameters).
\subsection{Recursive functions}\label{sec:recursion}
@@ -858,7 +855,7 @@
\end{rail}
-\subsubsection{Cases and induction: emulating tactic scripts}\label{sec:zf-induct-tac}
+\subsubsection{Cases and induction: emulating tactic scripts}
The following important tactical tools of Isabelle/ZF have been ported to
Isar. These should be never used in proper proof texts!
--- a/doc-src/IsarRef/pure.tex Thu Mar 07 22:52:07 2002 +0100
+++ b/doc-src/IsarRef/pure.tex Thu Mar 07 23:21:19 2002 +0100
@@ -1194,6 +1194,7 @@
\end{rail}
\begin{descr}
+
\item [$\APPLY{m}$] applies proof method $m$ in initial position, but unlike
$\PROOFNAME$ it retains ``$proof(prove)$'' mode. Thus consecutive method
applications may be given just as in tactic scripts.
@@ -1229,6 +1230,7 @@
$\isarkeyword{lemmas}$ (cf.\ \S\ref{sec:axms-thms}), so
$\isarkeyword{declare}$ only has the effect of applying attributes as
included in the theorem specification.
+
\end{descr}
Any proper Isar proof method may be used with tactic script commands such as
--- a/doc-src/isar.sty Thu Mar 07 22:52:07 2002 +0100
+++ b/doc-src/isar.sty Thu Mar 07 23:21:19 2002 +0100
@@ -30,7 +30,7 @@
\newcommand{\isaratt}{attribute}
\newcommand{\I@optname}[1]{\ifthenelse{\equal{}{#1}}{}{~#1\colon}}
-\newcommand{\I@optmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~(#1)}}
+\newcommand{\I@optmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~#1}}
\newcommand{\AND}{\isarkeyword{and}}
\newcommand{\IN}{\isarkeyword{in}}