ANNOUNCE
author chaieb
Thu, 14 Jun 2007 22:59:42 +0200
changeset 23392 4b03e3586f7f
parent 17696 eccdee8a0790
child 24802 6bd8ec8f3fc8
permissions -rw-r--r--
fixed term_constants (impact on is_relevant); terms in generalize_tac are sorted before we abstract over them (to *try* to avoid the case when a term to be abstracted over already occurs in an other)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17544
929d157d4369 updated for Isabelle2005;
wenzelm
parents: 14624
diff changeset
     1
Subject: Announcing Isabelle2005
9928
b7698bd95a94 template;
wenzelm
parents:
diff changeset
     2
To: isabelle-users@cl.cam.ac.uk
b7698bd95a94 template;
wenzelm
parents:
diff changeset
     3
17544
929d157d4369 updated for Isabelle2005;
wenzelm
parents: 14624
diff changeset
     4
Isabelle2005 is now available.
929d157d4369 updated for Isabelle2005;
wenzelm
parents: 14624
diff changeset
     5
17572
wenzelm
parents: 17544
diff changeset
     6
This release provides substantial advances over Isabelle2004, see the
wenzelm
parents: 17544
diff changeset
     7
first 1000 lines of NEWS in the distribution for more details.  Some
17692
6d277e731096 revert 'defs' advertisement;
wenzelm
parents: 17684
diff changeset
     8
highlights are:
17544
929d157d4369 updated for Isabelle2005;
wenzelm
parents: 14624
diff changeset
     9
929d157d4369 updated for Isabelle2005;
wenzelm
parents: 14624
diff changeset
    10
* Interpretation of locale expressions in theories, locales, and proof
929d157d4369 updated for Isabelle2005;
wenzelm
parents: 14624
diff changeset
    11
contexts.
929d157d4369 updated for Isabelle2005;
wenzelm
parents: 14624
diff changeset
    12
929d157d4369 updated for Isabelle2005;
wenzelm
parents: 14624
diff changeset
    13
* Substantial library improvements (HOL, HOL-Complex, HOLCF).
12927
wenzelm
parents: 11600
diff changeset
    14
17544
929d157d4369 updated for Isabelle2005;
wenzelm
parents: 14624
diff changeset
    15
* Proof tools for transitivity reasoning.
929d157d4369 updated for Isabelle2005;
wenzelm
parents: 14624
diff changeset
    16
929d157d4369 updated for Isabelle2005;
wenzelm
parents: 14624
diff changeset
    17
* General 'find_theorems' command (by term patterns, as
929d157d4369 updated for Isabelle2005;
wenzelm
parents: 14624
diff changeset
    18
intro/elim/simp rules etc.).
929d157d4369 updated for Isabelle2005;
wenzelm
parents: 14624
diff changeset
    19
17692
6d277e731096 revert 'defs' advertisement;
wenzelm
parents: 17684
diff changeset
    20
* Commands for generating ad-hoc draft documents.
17544
929d157d4369 updated for Isabelle2005;
wenzelm
parents: 14624
diff changeset
    21
929d157d4369 updated for Isabelle2005;
wenzelm
parents: 14624
diff changeset
    22
* Support for Unicode proof documents (UTF-8).
929d157d4369 updated for Isabelle2005;
wenzelm
parents: 14624
diff changeset
    23
929d157d4369 updated for Isabelle2005;
wenzelm
parents: 14624
diff changeset
    24
* Major internal reorganizations and performance improvements.
12927
wenzelm
parents: 11600
diff changeset
    25
12983
7d13480ee668 more stuff;
wenzelm
parents: 12964
diff changeset
    26
17544
929d157d4369 updated for Isabelle2005;
wenzelm
parents: 14624
diff changeset
    27
You may get Isabelle2005 from the following mirror sites:
9928
b7698bd95a94 template;
wenzelm
parents:
diff changeset
    28
17696
eccdee8a0790 adjusted www links
haftmann
parents: 17692
diff changeset
    29
  Cambridge (UK)       http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
eccdee8a0790 adjusted www links
haftmann
parents: 17692
diff changeset
    30
  Munich (Germany)     http://isabelle.in.tum.de/
14616
b167b1b848d8 added sydney mirror
kleing
parents: 14614
diff changeset
    31
  Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/