ANNOUNCE
author haftmann
Wed Sep 28 14:16:34 2005 +0200 (2005-09-28 ago)
changeset 17696 eccdee8a0790
parent 17692 6d277e731096
child 24802 6bd8ec8f3fc8
permissions -rw-r--r--
adjusted www links
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@17692
     8
highlights 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@17692
    20
* Commands for generating ad-hoc 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@12983
    26
wenzelm@17544
    27
You may get Isabelle2005 from the following mirror sites:
wenzelm@9928
    28
haftmann@17696
    29
  Cambridge (UK)       http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
haftmann@17696
    30
  Munich (Germany)     http://isabelle.in.tum.de/
kleing@14616
    31
  Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/