[Cdd-commits] r1025 - in projects/science/trunk/debian-science: debian tasks

[CDD Subversion Commit]

Author: sylvestre-guest
Date: Mon Aug 11 18:08:24 2008
New Revision: 1025

Modified:
   projects/science/trunk/debian-science/debian/changelog
   projects/science/trunk/debian-science/tasks/mathematics
Log:
Isabelle Added

Modified: projects/science/trunk/debian-science/debian/changelog
==============================================================================
--- projects/science/trunk/debian-science/debian/changelog	(original)
+++ projects/science/trunk/debian-science/debian/changelog	Mon Aug 11 18:08:24 2008
@@ -1,6 +1,7 @@
 debian-science (0.4) unstable; urgency=low
 
   * vipec & electric packages moved to Suggest (Closes: #494264)
+  * Some applications / libraires added
 
  -- Sylvestre Ledru <sylvestre.ledru at inria.fr>  Mon, 11 Aug 2008 15:02:11 +0200
 

Modified: projects/science/trunk/debian-science/tasks/mathematics
==============================================================================
--- projects/science/trunk/debian-science/tasks/mathematics	(original)
+++ projects/science/trunk/debian-science/tasks/mathematics	Mon Aug 11 18:08:24 2008
@@ -57,7 +57,6 @@
  mathematics software. Also it includes interfaces for applications like 
  maxima, octave and many others.
 
-
 Depends: geogebra
 Homepage: http://www.geogebra.org/
 WNPP: 447584
@@ -69,3 +68,20 @@
  them dynamically afterwards. On the other hand, equations and coordinates
  can be entered directly.
 
+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-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.