The coming Isabelle2016-1 release is scheduled for December 2016. This spot is continuously updated to inform about the ongoing process of testing release candidates.

• On 07-Oct-2016 an informal snapshot Isabelle2016-1-RC0 was published.
• On 28-Oct-2016 the release candidate Isabelle2016-1-RC1 was published. Serious testing by users is now required, to expose remaining problems.
• On 06-Nov-2016 the release candidate Isabelle2016-1-RC2 was published. Various details have been consolidated.
• On 22-Nov-2016 the release candidate Isabelle2016-1-RC3 was published. More fine points have been consolidated. A component for the new experimental Nunchaku tool has been included.
• On 27-Nov-2016 the release candidate Isabelle2016-1-RC4 was published. It introduces the following important last-minute changes:
  1. Prover IDE: more aggressive flushing of machine-generated input
  2. Sledgehammer: MaSh is faster and less likely to hang seemingly forever
  3. fine-tuning of Isabelle/LaTeX typesetting
• On 08-Dec-2016 the release candidate Isabelle2016-1-RC5 was published, presumably the last one. It introduces the following important last-minute changes:
  1. more uniform automatic indentation (empty vs. non-empty lines)
  2. fewer tracing/warning messages in some proof tools

The Isabelle release process is subject to the laws of causality: release candidates can be modified, but the final release remains final. Testing needs to happen in the weeks before the final release, not after it.

The main forum for discussion of Isabelle2016-1 release candidates is on isabelle-users mailing list.

Update 13-Dec-2016: The final release of Isabelle2016-1 (December 2016) is now available from the Isabelle website. The above release candidates will disappear eventually.