tool: Isabelle2009-2

---

Language:	Isabelle
Version:	2009-2
Author:	Written by Lawrence C Paulson, Tobias Nipkow, and Makarius Wenzel
Location:	http://isabelle.in.tum.de/
Description:	Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle is developed at University of Cambridge (Larry Paulson), Technische Universität München (Tobias Nipkow) and Université Paris-Sud (Makarius Wenzel). Notable changes: Explicit proof terms for type class reasoning. Robust treatment of concrete syntax for different logical entities; mixfix syntax in local proof context. Type declarations and notation within local theory context. HOL: package for quotient types. HOL code generation: simple concept for abstract datatypes obeying invariants (e.g. red-black trees). HOL: new development of the Reals using Cauchy Sequences. HOL: reorganization of abstract algebra type class hierarchy. HOL: substantial reorganization of main library and related tools. HOLCF: reorganization of 'domain' package.
Ports:	Linux, Mac OS X (Leopard or Snow Leopard), and Windows (via Cygwin).
Requires:	Proof General - http://proofgeneral.inf.ed.ac.uk/ , XEmacs - http://www.xemacs.org
Contact:	http://isabelle.in.tum.de/overview.html
Updated:	2010/06/22

category: logic programming languages summary, or expanded.