wenzelm@57452: Subject: Announcing Isabelle2014
wenzelm@9928: To: isabelle-users@cl.cam.ac.uk
wenzelm@9928: 
wenzelm@57452: Isabelle2014 is now available.
wenzelm@57452: 
wenzelm@57452: This version significantly improves upon Isabelle2013-2, see the NEWS
wenzelm@57452: file in the distribution for more details.  Some highlights are:
wenzelm@44975: 
wenzelm@57452: * Improved Isabelle/jEdit Prover IDE: navigation, completion,
wenzelm@57452:   spell-checking, Query panel, Simplifier Trace panel.
wenzelm@47869: 
wenzelm@57504: * Support for auxiliary files within the Prover IDE, notably
wenzelm@57504:   Isabelle/ML.
wenzelm@54034: 
wenzelm@57452: * Support for official Standard ML within the Prover IDE,
wenzelm@57452:   independently of Isabelle theory and proof development.
wenzelm@54034: 
wenzelm@57452: * HOL: BNF datatypes and codatatypes within theory Main, with numerous
wenzelm@57452:   add-on tools.
wenzelm@54034: 
wenzelm@57452: * HOL tool enhancements: Nitpick, Sledgehammer.
wenzelm@57452: 
wenzelm@57452: * HOL: internal SAT solver "cdclite" with models and proof traces.
wenzelm@57452: 
wenzelm@57452: * HOL: updated SMT module, with support for SMT-LIB 2 and recent
wenzelm@57452:   versions of Z3, as well as CVC3, CVC4.
wenzelm@54034: 
wenzelm@57505: * HOL: numerous library enhancements: main HOL, HOL-Word,
wenzelm@57505:   HOL-Multivariate_Analysis, HOL-Probability.
wenzelm@57504: 
wenzelm@57511: * System integration: improved support of LaTeX on Windows platform.
wenzelm@57504: 
wenzelm@57452: * Updated and extended manuals: codegen, datatypes, implementation,
wenzelm@57452:   isar-ref, jedit, system.
wenzelm@54034: 
wenzelm@12983: 
wenzelm@57524: You may get Isabelle2014 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/