ANNOUNCE
author boehmes
Fri, 27 May 2011 16:45:24 +0200
changeset 43041 218e3943d504
parent 41605 7d035da21e9c
child 44801 a0459c50cfc9
permissions -rw-r--r--
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
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/