reintroduced crucial sorting accidentally lost in 962190eab40d
The Isabelle System DistributionVersion information This is some unidentified repository version of Isabelle. See the NEWS file in the distribution for details on user-relevant changes.Installation Isabelle works on the three main platform families: Linux, Windows, and Mac OS X. Completely integrated bundles including the full Isabelle sources, documentation, add-on tools and precompiled logic images for several platforms are available from the Isabelle web page. Some background information may be found in the Isabelle System Manual, distributed with the sources (directory doc).User interfaces Isabelle/jEdit is an advanced Prover IDE based on jEdit and Isabelle/Scala. It provides a metaphor of continuous proof checking of a versioned collection of theory sources, with instantaneous feedback in real-time and rich semantic markup associated with the formal text. The classic Isabelle user interface is Proof General by David Aspinall and others. It is a generic Emacs interface for proof assistants, including Isabelle. Its main feature is script management, with stepwise proof scripting and partial locking of the editor buffer.Other sources of information The Isabelle Page The Isabelle home page may be accessed from Cambridge, Munich, and Sydney: * http://www.cl.cam.ac.uk/research/hvg/Isabelle/ * http://isabelle.in.tum.de * http://mirror.cse.unsw.edu.au/pub/isabelle/index.html Mailing list The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum for Isabelle users to discuss problems and exchange information. To join, send a message to isabelle-users-request@cl.cam.ac.uk. Personal mail Lawrence C Paulson Computer Laboratory University of Cambridge JJ Thomson Avenue Cambridge CB3 0FD England E-mail: lcp@cl.cam.ac.uk Phone: +44-223-763500 Fax: +44-223-334748 or Tobias Nipkow Institut fuer Informatik Technische Universitaet Muenchen Boltzmannstr. 3 D-85748 Garching Germany E-mail: nipkow@in.tum.de Phone: +49-89-289-17302 Fax: +49-89-289-17307 _________________________________________________________________ Please report any problems you encounter. While we shall try to be helpful, we can accept no responsibility for the deficiencies of Isabelle and their consequences. _________________________________________________________________