Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
Subject: Announcing Isabelle2005To: isabelle-users@cl.cam.ac.ukIsabelle2005 is now available.This release provides substantial advances over Isabelle2004, see thefirst 1000 lines of NEWS in the distribution for more details. Somehighlights are:* Interpretation of locale expressions in theories, locales, and proofcontexts.* Substantial library improvements (HOL, HOL-Complex, HOLCF).* Proof tools for transitivity reasoning.* General 'find_theorems' command (by term patterns, asintro/elim/simp rules etc.).* Commands for generating ad-hoc draft documents.* Support for Unicode proof documents (UTF-8).* Major internal reorganizations and performance improvements.You may get Isabelle2005 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/