wenzelm@62016: Subject: Announcing Isabelle2016 wenzelm@9928: To: isabelle-users@cl.cam.ac.uk wenzelm@9928: wenzelm@62016: Isabelle2016 is now available. wenzelm@57452: wenzelm@62028: This version improves upon Isabelle2015 in many ways, see the NEWS file in the wenzelm@62028: distribution for further details. Some highlights are as follows: wenzelm@62028: wenzelm@62028: * Enhanced Isabelle/jEdit Prover IDE, with separate State versus Output panel wenzelm@62028: and more asynchronous task management within the prover/GUI. wenzelm@62028: wenzelm@62028: * Additional Isar language elements for structured statements and proofs. wenzelm@62028: wenzelm@62028: * Document language refinements, with Markdown-like text structure. wenzelm@60116: wenzelm@62028: * More Isabelle symbols in theory and document sources. wenzelm@62028: wenzelm@62028: * Pure/HOL: uniform treatment of overloaded constant definitions versus type wenzelm@62028: definitions; upgrade of HOL typedef to definitional principle. wenzelm@62028: wenzelm@62029: * HOL tool enhancements: Sledgehammer, Nitpick, Quickcheck, Transfer. wenzelm@62028: wenzelm@62064: * Many HOL library improvements, notably HOL-Multivariate_Analysis. wenzelm@62028: wenzelm@62029: * Upgrade to Poly/ML 5.6 with debugger IDE support (Isabelle/ML and Standard wenzelm@62029: ML), per-thread profiling, native Windows version (32bit and 64bit). wenzelm@54034: wenzelm@12983: wenzelm@62016: You may get Isabelle2016 from the following mirror sites: wenzelm@9928: haftmann@27085: Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ haftmann@17696: Munich (Germany) http://isabelle.in.tum.de/ kleing@14616: Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/