--- a/ANNOUNCE Mon Feb 05 14:30:55 2001 +0100
+++ b/ANNOUNCE Mon Feb 05 14:31:49 2001 +0100
@@ -1,63 +1,43 @@
-Subject: Announcing Isabelle99-1
+Subject: Announcing Isabelle99-2
To: isabelle-users@cl.cam.ac.uk
-Isabelle99-1 is now available. This release continues the line of
-Isabelle99, introducing numerous improvements, both internal and user
-visible.
+Isabelle99-2 is now available. This release continues the line of
+Isabelle99, introducing various improvements in robustness and
+usability.
-In particular, great care has been taken to improve robustness and
-ease use and installation of the complete Isabelle working
-environment. This includes Proof General user interface support, WWW
-presentation of theories and the Isabelle document preparation system.
-
-The most prominent highlights of Isabelle99-1 are as follows. See the
+The most prominent highlights of Isabelle99-2 are as follows. See the
NEWS file distributed with Isabelle for more details.
- * Isabelle/Isar improvements (Markus Wenzel)
- o Support of tactic-emulation scripts for easy porting of legacy ML
- scripts (see also the HOL/Lambda example).
- o Better support for scalable verification tasks (manage large
- contexts in induction, generalized existence reasoning etc.)
- o Hindley-Milner polymorphism for proof texts.
- o More robust document preparation, better LaTeX output due to
- fake math-mode.
- o Extended "Isabelle/Isar Reference Manual".
+ * Poly/ML 4.0 used by default
+ More robust, less disk space required.
+
+ * Pure/Simplifier (Stefan Berghofer)
+ Proper implementation as a derived rule, outside the kernel!
- * HOL/Algebra (Clemens Ballarin)
- Rings and univariate polynomials.
-
- * HOL/BCV (Tobias Nipkow)
- Generic model of bytecode verification.
+ * Isabelle/Isar (Markus Wenzel)
+ Numerous usability improvements, e.g. support for initial
+ schematic goals, failure prediction of subgoal statements,
+ handling of non-atomic statements in induction.
- * HOL/IMPP (David von Oheimb)
- Extension of IMP with local variables and mutually recursive procedures.
-
- * HOL/Isar_examples (Markus Wenzel)
- More examples, including a formulation of Hoare Logic in Isabelle/Isar.
+ * Improved document preparation (Markus Wenzel)
+ Near math-mode, sub/super scripts, more symbols etc.
- * HOL/Lambda (Stefan Berghofer and Tobias Nipkow)
- More on termination of simply-typed lambda-terms (Isar script).
+ * HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson,
+ Thomas M Rasmussen, Markus Wenzel)
+ A collection of generic theories to be used together with main HOL.
- * HOL/Lattice (Markus Wenzel)
- Lattices and orders in Isabelle/Isar.
-
- * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
- Cornelia Pusch)
- Formalization of a fragment of Java, together with a corresponding
- virtual machine and a specification of its bytecode verifier.
+ * HOL/Real and HOL/Hyperreal (Lawrence C Paulson and Jacques Fleuriot)
+ General cleanup, more on nonstandard real analysis.
- * HOL/NumberTheory (Thomas Rasmussen)
- Fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
- Fermat/Euler Theorem, Wilson's Theorem.
+ * HOL/Unix (Markus Wenzel)
+ Some Aspects of Unix file-system security; demonstrates
+ Isabelle/Isar in typical system modelling and verification tasks.
- * HOL/Prolog (David von Oheimb)
- A (bare-bones) implementation of Lambda-Prolog.
+ * HOL/Tutorial (Tobias Nipkow, Lawrence C Paulson)
+ Extended version of the Isabelle/HOL tutorial.
- * HOL/Real (Jacques Fleuriot)
- More on nonstandard real analysis.
-
-You may get Isabelle99-1 from any of the following mirror sites:
+You may get Isabelle99-2 from any of the following mirror sites:
Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
Munich (Germany) http://isabelle.in.tum.de/dist/
--- a/Admin/makedist Mon Feb 05 14:30:55 2001 +0100
+++ b/Admin/makedist Mon Feb 05 14:31:49 2001 +0100
@@ -36,10 +36,10 @@
function usage()
{
- echo "###"
- echo "### Usage: $PRG VERSION"
- echo "###"
cat <<EOF
+
+Usage: $PRG VERSION
+
Make Isabelle distribution from the master sources at TUM.
VERSION may be either a tag like "Isabelle99-XX" that specifies the
@@ -49,22 +49,12 @@
Checklist for official releases (before running this script):
- * Check release name and date in NEWS!
- * Check that README files are up to date (should have Id: lines).
- * Check Admin/index.html.
-EOF
- #Wicked! We just won't tell other users ...
- if [ $LOGNAME = paulson -o $LOGNAME = nipkow -o $LOGNAME = wenzelm -o $LOGNAME = berghofe ]; then
- cat <<EOF
+ * Check Admin/page contents.
+ * Check ANNOUNCE, README, INSTALL, NEWS.
+ * Try "isatool makeall all" with Poly/ML, SML/NJ, etc.
* Tag the current repository version, e.g.:
cvs -d /usr/proj/isabelle-repository/archive rtag Isabelle99-X isabelle
- PLEASE DON'T DO THIS UNLESS YOU KNOW WHAT YOU'RE DOING!
-EOF
- fi
- cat <<EOF
-
- After the distribution has been created succesfully, you might want
- to run some makeall tests using different ML systems.
+ PLEASE DO NOT DO THIS UNLESS YOU KNOW WHAT YOU ARE DOING!
EOF
exit 1
--- a/Admin/page/dist-content/packages.content Mon Feb 05 14:30:55 2001 +0100
+++ b/Admin/page/dist-content/packages.content Mon Feb 05 14:31:49 2001 +0100
@@ -106,19 +106,8 @@
<p>
-The installation may be finished as follows:
-
-<p>
-
-<tt>
- <!-- _GP_ "cd /usr/local/" . distname --> <br>
- ./bin/isatool install -p /usr/local/bin <br>
-</tt>
-
-<p>
-
-Users can now invoke the Isabelle executables without further ado,
-e.g. just start the main <tt>Isabelle</tt> executable to lauch the
+Users may now invoke Isabelle without further ado, e.g. run the main
+executable <tt>/usr/local/Isabelle/bin/Isabelle</tt> to launch the
Isabelle Proof General interface.
<p>
--- a/NEWS Mon Feb 05 14:30:55 2001 +0100
+++ b/NEWS Mon Feb 05 14:31:49 2001 +0100
@@ -2,6 +2,9 @@
Isabelle NEWS -- history user-relevant changes
==============================================
+New in Isabelle99-2 (February 2001)
+-----------------------------------
+
*** Overview of INCOMPATIBILITIES ***
* HOL: inductive package no longer splits induction rule aggressively,
@@ -45,7 +48,7 @@
like this: "A\<^sup>*" or "A\<^sup>\<star>";
* some more standard symbols; see Appendix A of the system manual for
-the complete list;
+the complete list of symbols defined in isabellesym.sty;
* improved isabelle style files; more abstract symbol implementation
(should now use \isamath{...} and \isatext{...} in custom symbol
@@ -56,11 +59,14 @@
actual human-readable proof documents. Please do not include goal
states into document output unless you really know what you are doing!
-* isatool unsymbolize tunes sources for plain ASCII communication;
+* proper indentation of antiquoted output with proportional LaTeX
+fonts;
* no_document ML operator temporarily disables LaTeX document
generation;
+* isatool unsymbolize tunes sources for plain ASCII communication;
+
*** Isar ***
@@ -159,7 +165,7 @@
* print modes "brackets" and "no_brackets" control output of nested =>
(types) and ==> (props); the default behaviour is "brackets";
-* system: support Poly/ML 4.0 (current beta versions);
+* system: support Poly/ML 4.0;
* Pure: the Simplifier has been implemented properly as a derived rule
outside of the actual kernel (at last!); the overall performance
--- a/etc/settings Mon Feb 05 14:30:55 2001 +0100
+++ b/etc/settings Mon Feb 05 14:31:49 2001 +0100
@@ -42,18 +42,18 @@
#ML_OPTIONS="@SMLdebug=/dev/null"
#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
+# MLWorks 2.0
+#ML_SYSTEM=mlworks
+#ML_HOME="$ISABELLE_HOME/../mlworks/bin"
+#ML_OPTIONS=""
+#ML_PLATFORM=""
+
# Moscow ML 2.00 or later (experimental!)
#ML_SYSTEM=mosml
#ML_HOME="$ISABELLE_HOME/../mosml/bin"
#ML_PLATFORM=""
#ML_OPTIONS=""
-# MLWorks 2.0
-#ML_SYSTEM=mlworks
-#ML_HOME="$ISABELLE_HOME/../mlworks/bin"
-#ML_OPTIONS=""
-#ML_PLATFORM=""
-
# Standard ML of New Jersey 0.93
#ML_SYSTEM=smlnj-0.93
#ML_HOME=/usr/local/ldist/DIR/sml-0.93/src
@@ -79,8 +79,11 @@
ISABELLE_BIBTEX="bibtex"
ISABELLE_DVIPS="dvips -D 600"
+# Paranoia setting ...
+#unset TEXMF
+
# The thumbpdf tool is probably not generally available ...
-#ISABELLE_THUMBPDF="thumbpdf"
+#type -path thumbpdf >/dev/null && ISABELLE_THUMBPDF="thumbpdf"
###
@@ -175,7 +178,7 @@
"/usr/local/x-symbol" \
"/opt/x-symbol" \
"")
-#required for remote fonts only ...
+# Required for remote fonts only ...
#XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
--- a/etc/user-settings.sample Mon Feb 05 14:30:55 2001 +0100
+++ b/etc/user-settings.sample Mon Feb 05 14:31:49 2001 +0100
@@ -1,11 +1,7 @@
-#
+# -*- shell-script -*-
# $Id$
-# Author: Markus Wenzel, TU Muenchen
-# License: GPL (GNU GENERAL PUBLIC LICENSE)
#
-# Isabelle user settings sample (everything commented out)
-# -- may be copied to ~/isabelle/etc/settings
-#
+# Isabelle user settings sample -- may be copied to ~/isabelle/etc/settings
ISABELLE_USEDIR_OPTIONS="-i true -d pdf"
ISABELLE_LOGIC=HOL