ANNOUNCE

renamed functions from sizelim to more natural name depth_limited for compilation of depth-limited search in the predicate compiler

+
−Subject: Announcing Isabelle2009
+
−To: [e-mail]
+
−
+
−Isabelle2009 is now available.
+
−
+
−This release significantly improves upon Isabelle2008, see the NEWS
+
−file in the distribution for more details.  Some important changes
+
−are:
+
−
+
−* Complete re-implementation of locales, with proper support for local
+
−syntax, and more general locale expressions.
+
−
+
−* New 'find_consts' and 'find_theorems' facilities, together with
+
−"auto solve" feature of toplevel goal statements.
+
−
+
−* HOL: reorganization of main logic images.
+
−
+
−* HOL: improved implementation of Sledgehammer, based on generic ATP
+
−manager; support for remote ATPs.
+
−
+
−* HOL: numerous library improvements.
+
−
+
−* Updated and extended versions of main reference manuals.
+
−
+
−* Simplified arrangement of Isabelle startup scripts and settings
+
−directory.
+
−
+
−* Simplified programming interfaces for all Isar language elements.
+
−
+
−* General high-level support for concurrent ML programming.
+
−
+
−* Parallel proof checking within Isar theories.
+
−
+
−* Haskabelle importer from Haskell source files to Isar theories.
+
−
+
−
+
−You may get Isabelle2009 from the following mirror sites:
+
−
+
−  Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
+
−  Munich (Germany)     http://isabelle.in.tum.de/
+
−  Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/