tuned;
authorwenzelm
Mon Feb 05 14:31:49 2001 +0100 (2001-02-05)
changeset 11062e86340dc1d28
parent 11061 9b9d48ce3b6c
child 11063 82578cdb76cf
tuned;
ANNOUNCE
Admin/makedist
Admin/page/dist-content/packages.content
NEWS
etc/settings
etc/user-settings.sample
     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 +  * Pure/Simplifier (Stefan Berghofer)
    1.38 +    Proper implementation as a derived rule, outside the kernel!
    1.39  
    1.40 -  * HOL/Algebra (Clemens Ballarin)
    1.41 -    Rings and univariate polynomials.
    1.42 -
    1.43 -  * HOL/BCV (Tobias Nipkow)
    1.44 -    Generic model of bytecode verification.
    1.45 +  * Isabelle/Isar (Markus Wenzel)
    1.46 +    Numerous usability improvements, e.g. support for initial
    1.47 +    schematic goals, failure prediction of subgoal statements,
    1.48 +    handling of non-atomic statements in induction.
    1.49  
    1.50 -  * HOL/IMPP (David von Oheimb)
    1.51 -    Extension of IMP with local variables and mutually recursive procedures.
    1.52 -
    1.53 -  * HOL/Isar_examples (Markus Wenzel)
    1.54 -    More examples, including a formulation of Hoare Logic in Isabelle/Isar.
    1.55 +  * Improved document preparation (Markus Wenzel)
    1.56 +    Near math-mode, sub/super scripts, more symbols etc.
    1.57  
    1.58 -  * HOL/Lambda (Stefan Berghofer and Tobias Nipkow)
    1.59 -    More on termination of simply-typed lambda-terms (Isar script).
    1.60 +  * HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson,
    1.61 +      Thomas M Rasmussen, Markus Wenzel)
    1.62 +    A collection of generic theories to be used together with main HOL.
    1.63  
    1.64 -  * HOL/Lattice (Markus Wenzel)
    1.65 -    Lattices and orders in Isabelle/Isar.
    1.66 -
    1.67 -  * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
    1.68 -    Cornelia Pusch)
    1.69 -    Formalization of a fragment of Java, together with a corresponding
    1.70 -    virtual machine and a specification of its bytecode verifier.
    1.71 +  * HOL/Real and HOL/Hyperreal (Lawrence C Paulson and Jacques Fleuriot)
    1.72 +    General cleanup, more on nonstandard real analysis.
    1.73  
    1.74 -  * HOL/NumberTheory (Thomas Rasmussen)
    1.75 -    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
    1.76 -    Fermat/Euler Theorem, Wilson's Theorem.
    1.77 +  * HOL/Unix (Markus Wenzel)
    1.78 +    Some Aspects of Unix file-system security; demonstrates
    1.79 +    Isabelle/Isar in typical system modelling and verification tasks.
    1.80  
    1.81 -  * HOL/Prolog (David von Oheimb)
    1.82 -    A (bare-bones) implementation of Lambda-Prolog.
    1.83 +  * HOL/Tutorial (Tobias Nipkow, Lawrence C Paulson)
    1.84 +    Extended version of the Isabelle/HOL tutorial.
    1.85  
    1.86 -  * HOL/Real (Jacques Fleuriot)
    1.87 -    More on nonstandard real analysis.
    1.88 -
    1.89 -You may get Isabelle99-1 from any of the following mirror sites:
    1.90 +You may get Isabelle99-2 from any of the following mirror sites:
    1.91  
    1.92    Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    1.93    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 -&nbsp;&nbsp; <!-- _GP_ "cd /usr/local/" . distname --> <br>
    3.13 -&nbsp;&nbsp; ./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 -#
     6.5 +# -*- shell-script -*-
     6.6  # $Id$
     6.7 -# Author: Markus Wenzel, TU Muenchen
     6.8 -# License: GPL (GNU GENERAL PUBLIC LICENSE)
     6.9  #
    6.10 -# Isabelle user settings sample (everything commented out)
    6.11 -#   -- may be copied to ~/isabelle/etc/settings
    6.12 -#
    6.13 +# Isabelle user settings sample -- may be copied to ~/isabelle/etc/settings
    6.14  
    6.15  ISABELLE_USEDIR_OPTIONS="-i true -d pdf"
    6.16  ISABELLE_LOGIC=HOL