# HG changeset patch # User wenzelm # Date 981379909 -3600 # Node ID e86340dc1d2866cdf1ed254ebe2cb4a69a680d06 # Parent 9b9d48ce3b6c8a06d1e6c7e9dc7737bfdff37019 tuned; diff -r 9b9d48ce3b6c -r e86340dc1d28 ANNOUNCE --- 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/ diff -r 9b9d48ce3b6c -r e86340dc1d28 Admin/makedist --- 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 < -The installation may be finished as follows: - -

- - -  
-   ./bin/isatool install -p /usr/local/bin
- - -

- -Users can now invoke the Isabelle executables without further ado, -e.g. just start the main Isabelle executable to lauch the +Users may now invoke Isabelle without further ado, e.g. run the main +executable /usr/local/Isabelle/bin/Isabelle to launch the Isabelle Proof General interface.

diff -r 9b9d48ce3b6c -r e86340dc1d28 NEWS --- 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>\"; * 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 diff -r 9b9d48ce3b6c -r e86340dc1d28 etc/settings --- 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" diff -r 9b9d48ce3b6c -r e86340dc1d28 etc/user-settings.sample --- 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