ANNOUNCE
author wenzelm
Tue, 19 Apr 2011 15:58:05 +0200
changeset 42403 38b29c9fc742
parent 41605 7d035da21e9c
child 44801 a0459c50cfc9
permissions -rw-r--r--
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41604
313b0033034a some announcement;
wenzelm
parents: 37353
diff changeset
     1
Subject: Announcing Isabelle2011
9928
b7698bd95a94 template;
wenzelm
parents:
diff changeset
     2
To: isabelle-users@cl.cam.ac.uk
b7698bd95a94 template;
wenzelm
parents:
diff changeset
     3
41604
313b0033034a some announcement;
wenzelm
parents: 37353
diff changeset
     4
Isabelle2011 is now available.
17544
929d157d4369 updated for Isabelle2005;
wenzelm
parents: 14624
diff changeset
     5
41604
313b0033034a some announcement;
wenzelm
parents: 37353
diff changeset
     6
This version significantly improves upon Isabelle2009-2, see the NEWS
313b0033034a some announcement;
wenzelm
parents: 37353
diff changeset
     7
file in the distribution for more details.  Some notable changes are:
27007
c1960cad5017 added some notable improvements;
wenzelm
parents: 27005
diff changeset
     8
41604
313b0033034a some announcement;
wenzelm
parents: 37353
diff changeset
     9
* Experimental Prover IDE based on Isabelle/Scala and jEdit.
313b0033034a some announcement;
wenzelm
parents: 37353
diff changeset
    10
313b0033034a some announcement;
wenzelm
parents: 37353
diff changeset
    11
* Coercive subtyping (configured in HOL/Complex_Main).
37317
5164c4ec787b first proposal for a announcement
haftmann
parents: 37159
diff changeset
    12
41604
313b0033034a some announcement;
wenzelm
parents: 37353
diff changeset
    13
* HOL code generation: Scala as another target language.
37317
5164c4ec787b first proposal for a announcement
haftmann
parents: 37159
diff changeset
    14
41604
313b0033034a some announcement;
wenzelm
parents: 37353
diff changeset
    15
* HOL: partial_function definitions.
37353
b6222a65bacf tuned ANNOUNCEMENT;
wenzelm
parents: 37317
diff changeset
    16
41604
313b0033034a some announcement;
wenzelm
parents: 37353
diff changeset
    17
* HOL: various tool enhancements, including Quickcheck, Nitpick,
313b0033034a some announcement;
wenzelm
parents: 37353
diff changeset
    18
  Sledgehammer, SMT integration.
33873
e9120a7b2779 more tuning for release;
wenzelm
parents: 33866
diff changeset
    19
41604
313b0033034a some announcement;
wenzelm
parents: 37353
diff changeset
    20
* HOL: various additions to theory library, including HOL-Algebra,
41605
wenzelm
parents: 41604
diff changeset
    21
  Imperative_HOL, Multivariate_Analysis, Probability.
37317
5164c4ec787b first proposal for a announcement
haftmann
parents: 37159
diff changeset
    22
41604
313b0033034a some announcement;
wenzelm
parents: 37353
diff changeset
    23
* HOLCF: reorganization of library and related tools.
37317
5164c4ec787b first proposal for a announcement
haftmann
parents: 37159
diff changeset
    24
41604
313b0033034a some announcement;
wenzelm
parents: 37353
diff changeset
    25
* HOL/SPARK: interactive proof environment for verification conditions
313b0033034a some announcement;
wenzelm
parents: 37353
diff changeset
    26
  generated by the SPARK Ada program verifier.
37353
b6222a65bacf tuned ANNOUNCEMENT;
wenzelm
parents: 37317
diff changeset
    27
41604
313b0033034a some announcement;
wenzelm
parents: 37353
diff changeset
    28
* Improved Isabelle/Isar implementation manual (covering Isabelle/ML).
37353
b6222a65bacf tuned ANNOUNCEMENT;
wenzelm
parents: 37317
diff changeset
    29
12983
7d13480ee668 more stuff;
wenzelm
parents: 12964
diff changeset
    30
41604
313b0033034a some announcement;
wenzelm
parents: 37353
diff changeset
    31
You may get Isabelle2011 from the following mirror sites:
9928
b7698bd95a94 template;
wenzelm
parents:
diff changeset
    32
27085
dbf4f791953d adjusted location of cambridge website
haftmann
parents: 27066
diff changeset
    33
  Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
17696
eccdee8a0790 adjusted www links
haftmann
parents: 17692
diff changeset
    34
  Munich (Germany)     http://isabelle.in.tum.de/
14616
b167b1b848d8 added sydney mirror
kleing
parents: 14614
diff changeset
    35
  Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/