isabelle: ANNOUNCE@ae4dc5ac983f (annotated)

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 c2a2be496f35 tuned; wenzelm parents: 74680 diff changeset	41	* System: update to current Java 17 LTS.
c2a2be496f35 tuned; wenzelm parents: 74680 diff changeset	42
c2a2be496f35 tuned; 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

author	blanchet
	Mon, 31 Jan 2022 16:09:23 +0100
changeset 75031	ae4dc5ac983f
parent 74913	c2a2be496f35
child 76108	bdab17df07a9
permissions	-rw-r--r--