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

ANNOUNCE

author | haftmann |

Mon Sep 26 07:56:54 2016 +0200 (2016-09-26) | |

changeset 63950 | cdc1e59aa513 |

parent 62197 | f354900ac0ea |

child 64072 | 9f96e4da3064 |

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

syntactic type class for operation mod named after mod;

simplified assumptions of type class semiring_div

simplified assumptions of type class semiring_div

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