Bug#494491: ITP: isabelle -- Generic theorem proving environment
Good news ! Someone already have a repository: deb http://kisogawa.inf.ethz.ch/isamorph/debian/ testing main It may worth have a look at it... PS : Same for PolyML (Bug#494488: ITP: polyml). -- cheers, Loïc Fejoz Lionel Elie Mamane a écrit : Package: wnpp Severity: wishlist Owner: Lionel Elie Mamane [EMAIL PROTECTED], [EMAIL PROTECTED] * 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 -- To UNSUBSCRIBE, email to [EMAIL PROTECTED] with a subject of unsubscribe. Trouble? Contact [EMAIL PROTECTED]
Bug#494491: ITP: isabelle -- Generic theorem proving environment
On Mon, Aug 11, 2008 at 10:08:44AM +0200, Loïc Fejoz wrote: Someone already have a repository: deb http://kisogawa.inf.ethz.ch/isamorph/debian/ testing main It may worth have a look at it... Actually, Achim also has a repository http://www.brucker.ch/projects/debian/index.en.html. We are using those as a starting point. Thank you for the pointer, though. These packages are not quite ready for Debian, but we are working on it. -- Lionel -- To UNSUBSCRIBE, email to [EMAIL PROTECTED] with a subject of unsubscribe. Trouble? Contact [EMAIL PROTECTED]
Bug#494491: ITP: isabelle -- Generic theorem proving environment
Package: wnpp Severity: wishlist Owner: Lionel Elie Mamane [EMAIL PROTECTED], [EMAIL PROTECTED] * 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 -- To UNSUBSCRIBE, email to [EMAIL PROTECTED] with a subject of unsubscribe. Trouble? Contact [EMAIL PROTECTED]
