Added a second timeout mechanism to Refute.
For some reason, TimeLimit.timeLimit often does not work, and it
leaves Refute running forever, making any evaluation using
Mutabelle or Mirabelle impossible. The redundant timeout seems to
do the trick.
Subject: Announcing Isabelle2008
To: isabelle-users@cl.cam.ac.uk
Isabelle2008 is now available.
This release consolidates Isabelle2007, see the NEWS file in the
distribution for more details. Some notable improvements are:
* HOL: significant speedup of Metis prover; proper support for
multithreading.
* HOL: new version of 'primrec' command supporting type-inference and
local theory targets.
* HOL: improved support for termination proofs of recursive function
definitions.
* New local theory targets for class instantiation and overloading.
* Support for named dynamic lists of theorems.
* Simple TTY interface with command-line editing.
* Improved support for the Cygwin platform (Windows).
* Support for Poly/ML 5.2 with improved handling of multithreading and
external processes.
* Reorganized and updated version of Isabelle/Isar Reference Manual.
You may get Isabelle2008 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/