summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

ANNOUNCE

author | wenzelm |

Sat May 14 19:49:10 2016 +0200 (2016-05-14 ago) | |

changeset 63094 | 056ea294c256 |

parent 62197 | f354900ac0ea |

child 64072 | 9f96e4da3064 |

permissions | -rw-r--r-- |

toplevel theorem statements support 'if'/'for' eigen-context;

1 Subject: Announcing Isabelle2016

2 To: isabelle-users@cl.cam.ac.uk

4 Isabelle2016 is now available.

6 This version improves upon Isabelle2015 in many ways, see the NEWS file in the

7 distribution for further details. Some highlights are as follows:

9 * Enhanced Isabelle/jEdit Prover IDE, with separate State versus Output panel

10 and more asynchronous task management within the prover/GUI.

12 * Additional Isar language elements for structured statements and proofs.

14 * Document language refinements, with Markdown-like text structure.

16 * More Isabelle symbols in theory and document sources.

18 * Pure/HOL: uniform treatment of overloaded constant definitions versus type

19 definitions; upgrade of HOL typedef to definitional principle.

21 * HOL tool enhancements: Sledgehammer, Nitpick, Quickcheck, Transfer.

23 * HOL library additions and improvements, notably HOL-Multivariate_Analysis,

24 HOL-Probability, HOL-Data_Structures.

26 * Upgrade to Poly/ML 5.6 with debugger IDE support (Isabelle/ML and Standard

27 ML), per-thread profiling, native Windows version (32bit and 64bit).

30 You may get Isabelle2016 from the following mirror sites:

32 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle

33 Munich (Germany) http://isabelle.in.tum.de

34 Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle

35 Potsdam, NY (USA) http://mirror.clarkson.edu/isabelle