1.1 --- a/ANNOUNCE Mon Feb 05 14:30:55 2001 +0100
1.2 +++ b/ANNOUNCE Mon Feb 05 14:31:49 2001 +0100
1.3 @@ -1,63 +1,43 @@
1.4
1.5 -Subject: Announcing Isabelle99-1
1.6 +Subject: Announcing Isabelle99-2
1.7 To: isabelle-users@cl.cam.ac.uk
1.8
1.9 -Isabelle99-1 is now available. This release continues the line of
1.10 -Isabelle99, introducing numerous improvements, both internal and user
1.11 -visible.
1.12 +Isabelle99-2 is now available. This release continues the line of
1.13 +Isabelle99, introducing various improvements in robustness and
1.14 +usability.
1.15
1.16 -In particular, great care has been taken to improve robustness and
1.17 -ease use and installation of the complete Isabelle working
1.18 -environment. This includes Proof General user interface support, WWW
1.19 -presentation of theories and the Isabelle document preparation system.
1.20 -
1.21 -The most prominent highlights of Isabelle99-1 are as follows. See the
1.22 +The most prominent highlights of Isabelle99-2 are as follows. See the
1.23 NEWS file distributed with Isabelle for more details.
1.24
1.25 - * Isabelle/Isar improvements (Markus Wenzel)
1.26 - o Support of tactic-emulation scripts for easy porting of legacy ML
1.27 - scripts (see also the HOL/Lambda example).
1.28 - o Better support for scalable verification tasks (manage large
1.29 - contexts in induction, generalized existence reasoning etc.)
1.30 - o Hindley-Milner polymorphism for proof texts.
1.31 - o More robust document preparation, better LaTeX output due to
1.32 - fake math-mode.
1.33 - o Extended "Isabelle/Isar Reference Manual".
1.34 + * Poly/ML 4.0 used by default
1.35 + More robust, less disk space required.
1.36
1.37 - * HOL/Algebra (Clemens Ballarin)
1.38 - Rings and univariate polynomials.
1.39 + * Pure/Simplifier (Stefan Berghofer)
1.40 + Proper implementation as a derived rule, outside the kernel!
1.41
1.42 - * HOL/BCV (Tobias Nipkow)
1.43 - Generic model of bytecode verification.
1.44 + * Isabelle/Isar (Markus Wenzel)
1.45 + Numerous usability improvements, e.g. support for initial
1.46 + schematic goals, failure prediction of subgoal statements,
1.47 + handling of non-atomic statements in induction.
1.48
1.49 - * HOL/IMPP (David von Oheimb)
1.50 - Extension of IMP with local variables and mutually recursive procedures.
1.51 + * Improved document preparation (Markus Wenzel)
1.52 + Near math-mode, sub/super scripts, more symbols etc.
1.53
1.54 - * HOL/Isar_examples (Markus Wenzel)
1.55 - More examples, including a formulation of Hoare Logic in Isabelle/Isar.
1.56 + * HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson,
1.57 + Thomas M Rasmussen, Markus Wenzel)
1.58 + A collection of generic theories to be used together with main HOL.
1.59
1.60 - * HOL/Lambda (Stefan Berghofer and Tobias Nipkow)
1.61 - More on termination of simply-typed lambda-terms (Isar script).
1.62 + * HOL/Real and HOL/Hyperreal (Lawrence C Paulson and Jacques Fleuriot)
1.63 + General cleanup, more on nonstandard real analysis.
1.64
1.65 - * HOL/Lattice (Markus Wenzel)
1.66 - Lattices and orders in Isabelle/Isar.
1.67 + * HOL/Unix (Markus Wenzel)
1.68 + Some Aspects of Unix file-system security; demonstrates
1.69 + Isabelle/Isar in typical system modelling and verification tasks.
1.70
1.71 - * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
1.72 - Cornelia Pusch)
1.73 - Formalization of a fragment of Java, together with a corresponding
1.74 - virtual machine and a specification of its bytecode verifier.
1.75 + * HOL/Tutorial (Tobias Nipkow, Lawrence C Paulson)
1.76 + Extended version of the Isabelle/HOL tutorial.
1.77
1.78 - * HOL/NumberTheory (Thomas Rasmussen)
1.79 - Fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
1.80 - Fermat/Euler Theorem, Wilson's Theorem.
1.81 -
1.82 - * HOL/Prolog (David von Oheimb)
1.83 - A (bare-bones) implementation of Lambda-Prolog.
1.84 -
1.85 - * HOL/Real (Jacques Fleuriot)
1.86 - More on nonstandard real analysis.
1.87 -
1.88 -You may get Isabelle99-1 from any of the following mirror sites:
1.89 +You may get Isabelle99-2 from any of the following mirror sites:
1.90
1.91 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
1.92 Munich (Germany) http://isabelle.in.tum.de/dist/
2.1 --- a/Admin/makedist Mon Feb 05 14:30:55 2001 +0100
2.2 +++ b/Admin/makedist Mon Feb 05 14:31:49 2001 +0100
2.3 @@ -36,10 +36,10 @@
2.4
2.5 function usage()
2.6 {
2.7 - echo "###"
2.8 - echo "### Usage: $PRG VERSION"
2.9 - echo "###"
2.10 cat <<EOF
2.11 +
2.12 +Usage: $PRG VERSION
2.13 +
2.14 Make Isabelle distribution from the master sources at TUM.
2.15
2.16 VERSION may be either a tag like "Isabelle99-XX" that specifies the
2.17 @@ -49,22 +49,12 @@
2.18
2.19 Checklist for official releases (before running this script):
2.20
2.21 - * Check release name and date in NEWS!
2.22 - * Check that README files are up to date (should have Id: lines).
2.23 - * Check Admin/index.html.
2.24 -EOF
2.25 - #Wicked! We just won't tell other users ...
2.26 - if [ $LOGNAME = paulson -o $LOGNAME = nipkow -o $LOGNAME = wenzelm -o $LOGNAME = berghofe ]; then
2.27 - cat <<EOF
2.28 + * Check Admin/page contents.
2.29 + * Check ANNOUNCE, README, INSTALL, NEWS.
2.30 + * Try "isatool makeall all" with Poly/ML, SML/NJ, etc.
2.31 * Tag the current repository version, e.g.:
2.32 cvs -d /usr/proj/isabelle-repository/archive rtag Isabelle99-X isabelle
2.33 - PLEASE DON'T DO THIS UNLESS YOU KNOW WHAT YOU'RE DOING!
2.34 -EOF
2.35 - fi
2.36 - cat <<EOF
2.37 -
2.38 - After the distribution has been created succesfully, you might want
2.39 - to run some makeall tests using different ML systems.
2.40 + PLEASE DO NOT DO THIS UNLESS YOU KNOW WHAT YOU ARE DOING!
2.41
2.42 EOF
2.43 exit 1
3.1 --- a/Admin/page/dist-content/packages.content Mon Feb 05 14:30:55 2001 +0100
3.2 +++ b/Admin/page/dist-content/packages.content Mon Feb 05 14:31:49 2001 +0100
3.3 @@ -106,19 +106,8 @@
3.4
3.5 <p>
3.6
3.7 -The installation may be finished as follows:
3.8 -
3.9 -<p>
3.10 -
3.11 -<tt>
3.12 - <!-- _GP_ "cd /usr/local/" . distname --> <br>
3.13 - ./bin/isatool install -p /usr/local/bin <br>
3.14 -</tt>
3.15 -
3.16 -<p>
3.17 -
3.18 -Users can now invoke the Isabelle executables without further ado,
3.19 -e.g. just start the main <tt>Isabelle</tt> executable to lauch the
3.20 +Users may now invoke Isabelle without further ado, e.g. run the main
3.21 +executable <tt>/usr/local/Isabelle/bin/Isabelle</tt> to launch the
3.22 Isabelle Proof General interface.
3.23
3.24 <p>
4.1 --- a/NEWS Mon Feb 05 14:30:55 2001 +0100
4.2 +++ b/NEWS Mon Feb 05 14:31:49 2001 +0100
4.3 @@ -2,6 +2,9 @@
4.4 Isabelle NEWS -- history user-relevant changes
4.5 ==============================================
4.6
4.7 +New in Isabelle99-2 (February 2001)
4.8 +-----------------------------------
4.9 +
4.10 *** Overview of INCOMPATIBILITIES ***
4.11
4.12 * HOL: inductive package no longer splits induction rule aggressively,
4.13 @@ -45,7 +48,7 @@
4.14 like this: "A\<^sup>*" or "A\<^sup>\<star>";
4.15
4.16 * some more standard symbols; see Appendix A of the system manual for
4.17 -the complete list;
4.18 +the complete list of symbols defined in isabellesym.sty;
4.19
4.20 * improved isabelle style files; more abstract symbol implementation
4.21 (should now use \isamath{...} and \isatext{...} in custom symbol
4.22 @@ -56,11 +59,14 @@
4.23 actual human-readable proof documents. Please do not include goal
4.24 states into document output unless you really know what you are doing!
4.25
4.26 -* isatool unsymbolize tunes sources for plain ASCII communication;
4.27 +* proper indentation of antiquoted output with proportional LaTeX
4.28 +fonts;
4.29
4.30 * no_document ML operator temporarily disables LaTeX document
4.31 generation;
4.32
4.33 +* isatool unsymbolize tunes sources for plain ASCII communication;
4.34 +
4.35
4.36 *** Isar ***
4.37
4.38 @@ -159,7 +165,7 @@
4.39 * print modes "brackets" and "no_brackets" control output of nested =>
4.40 (types) and ==> (props); the default behaviour is "brackets";
4.41
4.42 -* system: support Poly/ML 4.0 (current beta versions);
4.43 +* system: support Poly/ML 4.0;
4.44
4.45 * Pure: the Simplifier has been implemented properly as a derived rule
4.46 outside of the actual kernel (at last!); the overall performance
5.1 --- a/etc/settings Mon Feb 05 14:30:55 2001 +0100
5.2 +++ b/etc/settings Mon Feb 05 14:31:49 2001 +0100
5.3 @@ -42,18 +42,18 @@
5.4 #ML_OPTIONS="@SMLdebug=/dev/null"
5.5 #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
5.6
5.7 +# MLWorks 2.0
5.8 +#ML_SYSTEM=mlworks
5.9 +#ML_HOME="$ISABELLE_HOME/../mlworks/bin"
5.10 +#ML_OPTIONS=""
5.11 +#ML_PLATFORM=""
5.12 +
5.13 # Moscow ML 2.00 or later (experimental!)
5.14 #ML_SYSTEM=mosml
5.15 #ML_HOME="$ISABELLE_HOME/../mosml/bin"
5.16 #ML_PLATFORM=""
5.17 #ML_OPTIONS=""
5.18
5.19 -# MLWorks 2.0
5.20 -#ML_SYSTEM=mlworks
5.21 -#ML_HOME="$ISABELLE_HOME/../mlworks/bin"
5.22 -#ML_OPTIONS=""
5.23 -#ML_PLATFORM=""
5.24 -
5.25 # Standard ML of New Jersey 0.93
5.26 #ML_SYSTEM=smlnj-0.93
5.27 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src
5.28 @@ -79,8 +79,11 @@
5.29 ISABELLE_BIBTEX="bibtex"
5.30 ISABELLE_DVIPS="dvips -D 600"
5.31
5.32 +# Paranoia setting ...
5.33 +#unset TEXMF
5.34 +
5.35 # The thumbpdf tool is probably not generally available ...
5.36 -#ISABELLE_THUMBPDF="thumbpdf"
5.37 +#type -path thumbpdf >/dev/null && ISABELLE_THUMBPDF="thumbpdf"
5.38
5.39
5.40 ###
5.41 @@ -175,7 +178,7 @@
5.42 "/usr/local/x-symbol" \
5.43 "/opt/x-symbol" \
5.44 "")
5.45 -#required for remote fonts only ...
5.46 +# Required for remote fonts only ...
5.47 #XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
5.48
5.49
6.1 --- a/etc/user-settings.sample Mon Feb 05 14:30:55 2001 +0100
6.2 +++ b/etc/user-settings.sample Mon Feb 05 14:31:49 2001 +0100
6.3 @@ -1,11 +1,7 @@
6.4 +# -*- shell-script -*-
6.5 +# $Id$
6.6 #
6.7 -# $Id$
6.8 -# Author: Markus Wenzel, TU Muenchen
6.9 -# License: GPL (GNU GENERAL PUBLIC LICENSE)
6.10 -#
6.11 -# Isabelle user settings sample (everything commented out)
6.12 -# -- may be copied to ~/isabelle/etc/settings
6.13 -#
6.14 +# Isabelle user settings sample -- may be copied to ~/isabelle/etc/settings
6.15
6.16 ISABELLE_USEDIR_OPTIONS="-i true -d pdf"
6.17 ISABELLE_LOGIC=HOL