ANNOUNCE
author wenzelm
Tue Sep 27 17:24:27 2005 +0200 (2005-09-27)
changeset 17684 c98508731bd6
parent 17572 81fcc0029761
child 17692 6d277e731096
permissions -rw-r--r--
more details about incomplete 'defs';
wenzelm@17544
     1
Subject: Announcing Isabelle2005
wenzelm@9928
     2
To: isabelle-users@cl.cam.ac.uk
wenzelm@9928
     3
wenzelm@17544
     4
Isabelle2005 is now available.
wenzelm@17544
     5
wenzelm@17572
     6
This release provides substantial advances over Isabelle2004, see the
wenzelm@17572
     7
first 1000 lines of NEWS in the distribution for more details.  Some
wenzelm@17684
     8
notable features are:
wenzelm@17544
     9
wenzelm@17544
    10
* Interpretation of locale expressions in theories, locales, and proof
wenzelm@17544
    11
contexts.
wenzelm@17544
    12
wenzelm@17544
    13
* Substantial library improvements (HOL, HOL-Complex, HOLCF).
wenzelm@12927
    14
wenzelm@17544
    15
* Proof tools for transitivity reasoning.
wenzelm@17544
    16
wenzelm@17544
    17
* General 'find_theorems' command (by term patterns, as
wenzelm@17544
    18
intro/elim/simp rules etc.).
wenzelm@17544
    19
wenzelm@17544
    20
* Commands for generating adhoc draft documents.
wenzelm@17544
    21
wenzelm@17544
    22
* Support for Unicode proof documents (UTF-8).
wenzelm@17544
    23
wenzelm@17544
    24
* Major internal reorganizations and performance improvements.
wenzelm@12927
    25
wenzelm@17684
    26
* 'defs': more checks for overloading, but less checks for cyclic
wenzelm@17684
    27
dependencies!
wenzelm@17684
    28
wenzelm@12983
    29
wenzelm@17544
    30
You may get Isabelle2005 from the following mirror sites:
wenzelm@9928
    31
kleing@14616
    32
  Cambridge (UK)       http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
kleing@14616
    33
  Munich (Germany)     http://isabelle.in.tum.de/dist/
kleing@14616
    34
  Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/