ANNOUNCE
author paulson
Tue, 17 Oct 2000 10:21:12 +0200
changeset 10231 178a272bceeb
parent 10168 50be659d4222
child 11062 e86340dc1d28
permissions -rw-r--r--
renaming of contrapos rules
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9928
b7698bd95a94 template;
wenzelm
parents:
diff changeset
     1
b7698bd95a94 template;
wenzelm
parents:
diff changeset
     2
Subject: Announcing Isabelle99-1
b7698bd95a94 template;
wenzelm
parents:
diff changeset
     3
To: isabelle-users@cl.cam.ac.uk
b7698bd95a94 template;
wenzelm
parents:
diff changeset
     4
10161
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
     5
Isabelle99-1 is now available.  This release continues the line of
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
     6
Isabelle99, introducing numerous improvements, both internal and user
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
     7
visible.
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
     8
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
     9
In particular, great care has been taken to improve robustness and
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    10
ease use and installation of the complete Isabelle working
10165
wenzelm
parents: 10162
diff changeset
    11
environment.  This includes Proof General user interface support, WWW
10161
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    12
presentation of theories and the Isabelle document preparation system.
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    13
10168
50be659d4222 final tuning;
wenzelm
parents: 10167
diff changeset
    14
The most prominent highlights of Isabelle99-1 are as follows.  See the
50be659d4222 final tuning;
wenzelm
parents: 10167
diff changeset
    15
NEWS file distributed with Isabelle for more details.
9928
b7698bd95a94 template;
wenzelm
parents:
diff changeset
    16
10161
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    17
  * Isabelle/Isar improvements (Markus Wenzel)
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    18
      o Support of tactic-emulation scripts for easy porting of legacy ML
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    19
        scripts (see also the HOL/Lambda example).
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    20
      o Better support for scalable verification tasks (manage large
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    21
        contexts in induction, generalized existence reasoning etc.)
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    22
      o Hindley-Milner polymorphism for proof texts.
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    23
      o More robust document preparation, better LaTeX output due to
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    24
        fake math-mode.
10166
wenzelm
parents: 10165
diff changeset
    25
      o Extended "Isabelle/Isar Reference Manual".
9928
b7698bd95a94 template;
wenzelm
parents:
diff changeset
    26
10166
wenzelm
parents: 10165
diff changeset
    27
  * HOL/Algebra (Clemens Ballarin)
wenzelm
parents: 10165
diff changeset
    28
    Rings and univariate polynomials.
10161
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    29
10162
wenzelm
parents: 10161
diff changeset
    30
  * HOL/BCV (Tobias Nipkow)
10168
50be659d4222 final tuning;
wenzelm
parents: 10167
diff changeset
    31
    Generic model of bytecode verification.
10162
wenzelm
parents: 10161
diff changeset
    32
10166
wenzelm
parents: 10165
diff changeset
    33
  * HOL/IMPP (David von Oheimb)
10168
50be659d4222 final tuning;
wenzelm
parents: 10167
diff changeset
    34
    Extension of IMP with local variables and mutually recursive procedures.
10161
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    35
10166
wenzelm
parents: 10165
diff changeset
    36
  * HOL/Isar_examples (Markus Wenzel)
wenzelm
parents: 10165
diff changeset
    37
    More examples, including a formulation of Hoare Logic in Isabelle/Isar.
10161
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    38
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    39
  * HOL/Lambda (Stefan Berghofer and Tobias Nipkow)
10168
50be659d4222 final tuning;
wenzelm
parents: 10167
diff changeset
    40
    More on termination of simply-typed lambda-terms (Isar script).
10161
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    41
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    42
  * HOL/Lattice (Markus Wenzel)
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    43
    Lattices and orders in Isabelle/Isar.
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    44
10166
wenzelm
parents: 10165
diff changeset
    45
  * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
wenzelm
parents: 10165
diff changeset
    46
    Cornelia Pusch)
wenzelm
parents: 10165
diff changeset
    47
    Formalization of a fragment of Java, together with a corresponding
10168
50be659d4222 final tuning;
wenzelm
parents: 10167
diff changeset
    48
    virtual machine and a specification of its bytecode verifier.
10166
wenzelm
parents: 10165
diff changeset
    49
wenzelm
parents: 10165
diff changeset
    50
  * HOL/NumberTheory (Thomas Rasmussen)
wenzelm
parents: 10165
diff changeset
    51
    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
wenzelm
parents: 10165
diff changeset
    52
    Fermat/Euler Theorem, Wilson's Theorem.
wenzelm
parents: 10165
diff changeset
    53
10161
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    54
  * HOL/Prolog (David von Oheimb)
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    55
    A (bare-bones) implementation of Lambda-Prolog.
9928
b7698bd95a94 template;
wenzelm
parents:
diff changeset
    56
10167
wenzelm
parents: 10166
diff changeset
    57
  * HOL/Real (Jacques Fleuriot)
wenzelm
parents: 10166
diff changeset
    58
    More on nonstandard real analysis.
10166
wenzelm
parents: 10165
diff changeset
    59
9928
b7698bd95a94 template;
wenzelm
parents:
diff changeset
    60
You may get Isabelle99-1 from any of the following mirror sites:
b7698bd95a94 template;
wenzelm
parents:
diff changeset
    61
b7698bd95a94 template;
wenzelm
parents:
diff changeset
    62
  Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
b7698bd95a94 template;
wenzelm
parents:
diff changeset
    63
  Munich (Germany)  http://isabelle.in.tum.de/dist/
10161
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    64
  New Jersey (USA)  ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    65
  Stanford (USA)    ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html