[Blends-commit] r3418 - /projects/science/trunk/debian-science/tasks/mathematics

[tille at users.alioth.debian.org]

Author: tille
Date: Wed Jun 13 14:00:57 2012
New Revision: 3418

URL: http://svn.debian.org/wsvn/blends/?sc=1&rev=3418
Log:
Remove extra information about package isabelle which is available in Vcs and add Remark about alternative package because upstream does not like packaging

Modified:
    projects/science/trunk/debian-science/tasks/mathematics

Modified: projects/science/trunk/debian-science/tasks/mathematics
URL: http://svn.debian.org/wsvn/blends/projects/science/trunk/debian-science/tasks/mathematics?rev=3418&op=diff
==============================================================================
--- projects/science/trunk/debian-science/tasks/mathematics (original)
+++ projects/science/trunk/debian-science/tasks/mathematics Wed Jun 13 14:00:57 2012
@@ -86,22 +86,9 @@
 Depends: freefem++
 
 Depends: isabelle
-Homepage: http://isabelle.in.tum.de/
-WNPP: 494491
-License: BSD-like and non-free documentation
-Responsible: Lionel Elie Mamane <lionel at mamane.lu>, brucker at member.fsf.org
-Pkg-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-Lof 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.
+Remark: upstream prefers Isabelle not being packaged
+ There is an alternative software coq which is packaged in
+ Debian (see above).
 
 Depends: bliss