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