[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Bug#494491: marked as done (ITP: isabelle -- Generic theorem proving environment)

Your message dated Fri, 24 Jul 2009 12:53:11 +0200
with message-id <20090724105311.GA28064@capsaicin.mamane.lu>
and subject line Not going to package Isabelle
has caused the Debian Bug report #494491,
regarding ITP: isabelle -- Generic theorem proving environment
to be marked as done.

This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.

(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact owner@bugs.debian.org
immediately.)


-- 
494491: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=494491
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message --- 
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

--- End Message ---
--- Begin Message --- 
We have given up on packaging Isabelle, for various technical and
social reasons.

-- 
Lionel

--- End Message ---
Reply to: