ANNOUNCE
author wenzelm
Fri, 19 Aug 2022 23:58:44 +0200
changeset 75916 b6589c8ccadd
parent 74913 c2a2be496f35
child 76108 bdab17df07a9
permissions -rw-r--r--
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
74651
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
     1
Subject: Announcing Isabelle2021-1
9928
b7698bd95a94 template;
wenzelm
parents:
diff changeset
     2
To: isabelle-users@cl.cam.ac.uk
b7698bd95a94 template;
wenzelm
parents:
diff changeset
     3
74651
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
     4
Isabelle2021-1 is now available.
60116
5d90d301ad66 ANNOUNCE material, based on NEWS;
wenzelm
parents: 60016
diff changeset
     5
74651
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
     6
This version introduces many changes over Isabelle2020-1: see the NEWS
73010
a569465f8b57 updated for release;
wenzelm
parents: 71491
diff changeset
     7
file for further details. Here are various details:
68545
7922992c99ea misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
     8
74680
b80a8d7db99d more to ANNOUNCE;
wenzelm
parents: 74651
diff changeset
     9
* HTML presentation now includes links to formal entities.
b80a8d7db99d more to ANNOUNCE;
wenzelm
parents: 74651
diff changeset
    10
74651
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    11
* Isar: local theory support for 'syntax' and 'no_syntax' commands.
73010
a569465f8b57 updated for release;
wenzelm
parents: 71491
diff changeset
    12
74651
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    13
* Isabelle/jEdit: distribution of original jEdit editor with Isabelle/Scala
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    14
modules and plugins.
68545
7922992c99ea misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    15
74651
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    16
* HOL: new order prover.
68545
7922992c99ea misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    17
74651
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    18
* HOL: many changes and improvements on bit operations and word types.
71485
29e297fd5473 updated for release;
wenzelm
parents: 70286
diff changeset
    19
74651
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    20
* HOL: various library improvements (HOL-Library, HOL-Combinatorics,
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    21
HOL-Analysis, HOL-Statespace)
68545
7922992c99ea misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    22
74651
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    23
* Sledgehammer: update of ATPs and SMTs: E prover, veriT, Zipperposition,
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    24
Vampire (now with Open-Source license).
68545
7922992c99ea misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    25
74651
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    26
* Nitpick: external MiniSat solver for all supported Isabelle platforms.
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    27
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    28
* ML: uniform treatment of external processes via Isabelle/Scala.
71485
29e297fd5473 updated for release;
wenzelm
parents: 70286
diff changeset
    29
74651
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    30
* ML: advanced antiquotations for Type/Const constructors, and for inline
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    31
instantiation of types, terms, facts.
68545
7922992c99ea misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    32
74651
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    33
* Haskell: substantially improved Isabelle/Haskell library.
68648
371e814af6f0 more ANNOUNCE;
wenzelm
parents: 68599
diff changeset
    34
74651
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    35
* System: more predefined Isabelle symbols (blackboard-bold, Z notation).
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    36
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    37
* System: support for Isabelle/Scala modules defined in user-space.
68648
371e814af6f0 more ANNOUNCE;
wenzelm
parents: 68599
diff changeset
    38
74651
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    39
* System: improved document preparation using Isabelle/Scala.
68545
7922992c99ea misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    40
74913
wenzelm
parents: 74680
diff changeset
    41
* System: update to current Java 17 LTS.
wenzelm
parents: 74680
diff changeset
    42
wenzelm
parents: 74680
diff changeset
    43
* System: update to Poly/ML 5.9 with improved support for ARM64 on Linux.
54034
07844b536810 some highlights of Isabelle2013-1 based on NEWS;
wenzelm
parents: 53978
diff changeset
    44
12983
7d13480ee668 more stuff;
wenzelm
parents: 12964
diff changeset
    45
74651
81cc8f2ea9e7 updated for release;
wenzelm
parents: 73232
diff changeset
    46
You may get Isabelle2021-1 from the following mirror sites:
9928
b7698bd95a94 template;
wenzelm
parents:
diff changeset
    47
68599
cc7b5e0355a5 prefer HTTPS;
wenzelm
parents: 68567
diff changeset
    48
  Cambridge (UK)       https://www.cl.cam.ac.uk/research/hvg/Isabelle
cc7b5e0355a5 prefer HTTPS;
wenzelm
parents: 68567
diff changeset
    49
  Munich (Germany)     https://isabelle.in.tum.de
70032
0674c24afc5e updated for release;
wenzelm
parents: 68648
diff changeset
    50
  Sydney (Australia)   https://mirror.cse.unsw.edu.au/pub/isabelle
68599
cc7b5e0355a5 prefer HTTPS;
wenzelm
parents: 68567
diff changeset
    51
  Potsdam, NY (USA)    https://mirror.clarkson.edu/isabelle