Bug#494491: ITP: isabelle -- Generic theorem proving environment

[Lionel Elie Mamane <lionel@mamane.lu>]

Package: wnpp
Severity: wishlist
Owner: Lionel Elie Mamane <lionel@mamane.lu>, brucker@member.fsf.org

* Package name    : isabelle
  Version         : 2008
  Upstream Author : University of Cambridge (Larry Paulson), Technische Universitaet Muenchen (Tobias Nipkow, Makarius Wenzel)
* URL             : http://isabelle.in.tum.de/, http://www.cl.cam.ac.uk/research/hvg/Isabelle/
* License         : 3-clause BSD-like
                    (non-free documentation)
  Programming Lang: Standard ML
  Description     : Generic theorem proving environment

 Features a choice of several ready-to-use logics (Higher Order Logic,
 Higher Order Logic augmented with Scott's Logic for Computable
 Functions, First Order Logic, Zermello-Frankel, an extensional
 version of Martin-Löf Type Theory, Barendregt's Lambda Cube, a few
 sequent calculi (including modal and linear logics), ...) or
 defining your own logic / deductive system, a procedural and a
 declarative proof style, rich automation for classical reasoning,
 equational logic and algebra, LaTeX and X-Symbols notational support.
 .
 Isabelle can also be used as a generic framework for rapid
 prototyping of deductive systems.

-- System Information:
Debian Release: lenny/sid
  APT prefers unstable
  APT policy: (500, 'unstable'), (1, 'experimental')
Architecture: amd64 (x86_64)

Kernel: Linux 2.6.25-2-amd64 (SMP w/2 CPU cores)
Locale: LANG=fr_LU.UTF-8, LC_CTYPE=fr_LU.UTF-8 (charmap=UTF-8)
Shell: /bin/sh linked to /bin/bash