1.1 --- a/ANNOUNCE	Thu Mar 07 22:52:07 2002 +0100
     1.2 +++ b/ANNOUNCE	Thu Mar 07 23:21:19 2002 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4      Isabelle2002 is the official version to go along with that book
     1.5      (by Tobias Nipkow, Larry Paulson, Markus Wenzel).
     1.6  
     1.7 -  * Pure: explicit proof terms for all internal inferences:
     1.8 +  * Pure: explicit proof terms for all internal inferences;
     1.9      object-logics, proof tools etc. will benefit automatically
    1.10      (by Stefan Berghofer).
    1.11  
    1.12 @@ -27,28 +27,30 @@
    1.13      operations, and type-inference for structured specifications
    1.14      (by Markus Wenzel).
    1.15  
    1.16 -  * Pure/Isar: streamlined induction proof patterns
    1.17 +  * Pure/Isar: streamlined cases/induction proof patterns
    1.18      (by Markus Wenzel).
    1.19  
    1.20    * Pure/HOL: infrastructure for generating functional and relational
    1.21 -    code, using the ML run-time environment (by Stefan Berghofer).
    1.22 +    code, using the ML run-time environment
    1.23 +    (by Stefan Berghofer).
    1.24  
    1.25 -  * HOL/library: numerals on all number types; several
    1.26 -    improvements of tuple and record types; new definite description
    1.27 -    operator; keep Hilbert's epsilon (Axiom of Choice) out of basic theories.
    1.28 +  * HOL/library: numerals on all number types; several improvements of
    1.29 +    tuple and record types; new definite description operator; keep
    1.30 +    Hilbert's epsilon (Axiom of Choice) out of basic theories
    1.31 +    (by Stefan Berghofer, Larry Paulson, Markus Wenzel).
    1.32  
    1.33    * HOL/Bali: large application concerning formal treatment of Java.
    1.34      (by David von Oheimb and Norbert Schirmer).
    1.35  
    1.36    * HOL/HoareParallel: large application concerning verification of
    1.37      parallel imperative programs (Owicki-Gries method, Rely-Guarantee
    1.38 -    method, examples of garbage collection, mutual exclusion, etc.)
    1.39 +    method, examples of garbage collection, mutual exclusion)
    1.40      (by Leonor Prensa Nieto).
    1.41  
    1.42    * HOL/GroupTheory: group theory examples including Sylow's theorem
    1.43 -    (by Florian Kammüller).
    1.44 +    (by Florian Kammueller).
    1.45  
    1.46 -  * HOL/IMP: new proofs in Isar format
    1.47 +  * HOL/IMP: several new proofs in Isar format
    1.48      (by Gerwin Klein).
    1.49  
    1.50    * HOL/MicroJava: exception handling on the bytecode level
    1.51 @@ -61,10 +63,8 @@
    1.52      (by Markus Wenzel).
    1.53  
    1.54    * System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting
    1.55 -    larger heap size of applications.
    1.56 -
    1.57 -  * System: support for MacOS X (for Poly/ML and SML/NJ).
    1.58 -
    1.59 +    larger heap size of applications; support for MacOS X (Poly/ML and
    1.60 +    SML/NJ).
    1.61  
    1.62  You may get Isabelle2002 from any of the following mirror sites:
    1.63  

     2.1 --- a/NEWS	Thu Mar 07 22:52:07 2002 +0100
     2.2 +++ b/NEWS	Thu Mar 07 23:21:19 2002 +0100
     2.3 @@ -210,7 +210,7 @@
     2.4  
     2.5    - remove all special provisions on numerals in proofs;
     2.6  
     2.7 -* HOL: simp rules nat_number_of expand numerals on nat to Suc/0
     2.8 +* HOL: simp rules nat_number expand numerals on nat to Suc/0
     2.9  representation (depends on bin_arith_simps in the default context);
    2.10  
    2.11  * HOL: symbolic syntax for x^2 (numeral 2);

     3.1 --- a/doc-src/IsarRef/conversion.tex	Thu Mar 07 22:52:07 2002 +0100
     3.2 +++ b/doc-src/IsarRef/conversion.tex	Thu Mar 07 23:21:19 2002 +0100
     3.3 @@ -188,7 +188,7 @@
     3.4  This may be replaced by using the $unfold$ proof method explicitly.
     3.5  \begin{matharray}{l}
     3.6  \LEMMA{name}{\texttt"{\phi}\texttt"} \\
     3.7 -\quad \APPLY{unfold~def@1~\dots} \\
     3.8 +\quad \APPLY{(unfold~def@1~\dots)} \\
     3.9  \end{matharray}
    3.10  
    3.11  
    3.12 @@ -224,7 +224,7 @@
    3.13  $simp$, $blast$, or $auto$.  This could work as follows:
    3.14  \begin{matharray}{l}
    3.15    \LEMMA{}{\texttt"{\phi@1 \Imp \dots \Imp \psi}\texttt"} \\
    3.16 -  \quad \BYY{unfold~defs}{blast} \\
    3.17 +  \quad \BYY{(unfold~defs)}{blast} \\
    3.18  \end{matharray}
    3.19  Note that classic Isabelle would support this form only in the special case
    3.20  where $\phi@1$, \dots are atomic statements (when using the standard
    3.21 @@ -265,7 +265,7 @@
    3.22  
    3.23  \begin{matharray}{l}
    3.24    \LEMMA{name}{\texttt"{\All{\vec x}\vec\phi \Imp \psi}\texttt"} \\
    3.25 -  \quad \APPLY{atomize~(full)} \\
    3.26 +  \quad \APPLY{(atomize~(full))} \\
    3.27    \quad \APPLY{meth@1} \\
    3.28    \qquad \vdots \\
    3.29    \quad \DONE \\

     4.1 --- a/doc-src/IsarRef/generic.tex	Thu Mar 07 22:52:07 2002 +0100
     4.2 +++ b/doc-src/IsarRef/generic.tex	Thu Mar 07 23:21:19 2002 +0100
     4.3 @@ -230,8 +230,8 @@
     4.4    \quad \PROOF{succeed} \\
     4.5    \qquad \FIX{thesis} \\
     4.6    \qquad \ASSUME{that~[intro?]}{\All{\vec x} \vec\phi \Imp thesis} \\
     4.7 -  \qquad \SHOW{}{thesis} \\
     4.8 -  \quad\qquad \APPLY{insert~that} \\
     4.9 +  \qquad \THUS{}{thesis} \\
    4.10 +  \quad\qquad \APPLY{-} \\
    4.11    \quad\qquad \USING{\vec b}~~\langle proof\rangle \\
    4.12    \quad \QED{} \\
    4.13    \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\

     5.1 --- a/doc-src/IsarRef/logics.tex	Thu Mar 07 22:52:07 2002 +0100
     5.2 +++ b/doc-src/IsarRef/logics.tex	Thu Mar 07 23:21:19 2002 +0100
     5.3 @@ -228,18 +228,16 @@
     5.4  \medskip
     5.5  
     5.6  In Isabelle/HOL record types have to be defined explicitly, fixing their field
     5.7 -names and types, and their (optional) parent record (see
     5.8 -{\S}\ref{sec:hol-record-def}).  Afterwards, records may be formed using above
     5.9 -syntax, while obeying the canonical order of fields as given by their
    5.10 -declaration.  The record package provides several standard operations like
    5.11 -selectors and updates (see {\S}\ref{sec:hol-record-ops}).  The common setup
    5.12 -for various generic proof tools enable succinct reasoning patterns (see
    5.13 -{\S}\ref{sec:hol-record-thms}).  See also the Isabelle/HOL tutorial
    5.14 -\cite{isabelle-hol-book} for further instructions on using records in
    5.15 +names and types, and their (optional) parent record.  Afterwards, records may
    5.16 +be formed using above syntax, while obeying the canonical order of fields as
    5.17 +given by their declaration.  The record package provides several standard
    5.18 +operations like selectors and updates.  The common setup for various generic
    5.19 +proof tools enable succinct reasoning patterns.  See also the Isabelle/HOL
    5.20 +tutorial \cite{isabelle-hol-book} for further instructions on using records in
    5.21  practice.
    5.22  
    5.23  
    5.24 -\subsubsection{Record specifications}\label{sec:hol-record-def}
    5.25 +\subsubsection{Record specifications}
    5.26  
    5.27  \indexisarcmdof{HOL}{record}
    5.28  \begin{matharray}{rcl}
    5.29 @@ -275,7 +273,7 @@
    5.30  
    5.31  \end{descr}
    5.32  
    5.33 -\subsubsection{Record operations}\label{sec:hol-record-ops}
    5.34 +\subsubsection{Record operations}
    5.35  
    5.36  Any record definition of the form presented above produces certain standard
    5.37  operations.  Selectors and updates are provided for any field, including the
    5.38 @@ -343,7 +341,7 @@
    5.39  \noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ actually coincide for root records.
    5.40  
    5.41  
    5.42 -\subsubsection{Derived rules and proof tools}\label{sec:hol-record-thms}
    5.43 +\subsubsection{Derived rules and proof tools}
    5.44  
    5.45  The record package proves several results internally, declaring these facts to
    5.46  appropriate proof tools.  This enables users to reason about record structures
    5.47 @@ -425,9 +423,8 @@
    5.48  old-style theory syntax being used there!  Apart from proper proof methods for
    5.49  case-analysis and induction, there are also emulations of ML tactics
    5.50  \texttt{case_tac} and \texttt{induct_tac} available, see
    5.51 -\S\ref{sec:hol-induct-tac} or \S\ref{sec:zf-induct-tac}; these admit to refer
    5.52 -directly to the internal structure of subgoals (including internally bound
    5.53 -parameters).
    5.54 +\S\ref{sec:hol-induct-tac}; these admit to refer directly to the internal
    5.55 +structure of subgoals (including internally bound parameters).
    5.56  
    5.57  
    5.58  \subsection{Recursive functions}\label{sec:recursion}
    5.59 @@ -858,7 +855,7 @@
    5.60  \end{rail}
    5.61  
    5.62  
    5.63 -\subsubsection{Cases and induction: emulating tactic scripts}\label{sec:zf-induct-tac}
    5.64 +\subsubsection{Cases and induction: emulating tactic scripts}
    5.65  
    5.66  The following important tactical tools of Isabelle/ZF have been ported to
    5.67  Isar.  These should be never used in proper proof texts!

     6.1 --- a/doc-src/IsarRef/pure.tex	Thu Mar 07 22:52:07 2002 +0100
     6.2 +++ b/doc-src/IsarRef/pure.tex	Thu Mar 07 23:21:19 2002 +0100
     6.3 @@ -1194,6 +1194,7 @@
     6.4  \end{rail}
     6.5  
     6.6  \begin{descr}
     6.7 +
     6.8  \item [$\APPLY{m}$] applies proof method $m$ in initial position, but unlike
     6.9    $\PROOFNAME$ it retains ``$proof(prove)$'' mode.  Thus consecutive method
    6.10    applications may be given just as in tactic scripts.
    6.11 @@ -1229,6 +1230,7 @@
    6.12    $\isarkeyword{lemmas}$ (cf.\ \S\ref{sec:axms-thms}), so
    6.13    $\isarkeyword{declare}$ only has the effect of applying attributes as
    6.14    included in the theorem specification.
    6.15 +
    6.16  \end{descr}
    6.17  
    6.18  Any proper Isar proof method may be used with tactic script commands such as

     7.1 --- a/doc-src/isar.sty	Thu Mar 07 22:52:07 2002 +0100
     7.2 +++ b/doc-src/isar.sty	Thu Mar 07 23:21:19 2002 +0100
     7.3 @@ -30,7 +30,7 @@
     7.4  \newcommand{\isaratt}{attribute}
     7.5  
     7.6  \newcommand{\I@optname}[1]{\ifthenelse{\equal{}{#1}}{}{~#1\colon}}
     7.7 -\newcommand{\I@optmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~(#1)}}
     7.8 +\newcommand{\I@optmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~#1}}
     7.9  
    7.10  \newcommand{\AND}{\isarkeyword{and}}
    7.11  \newcommand{\IN}{\isarkeyword{in}}