4 Maintainer: Enrico Tassi <gareuselesinge@debian.org>
5 Uploaders: Stefano Zacchiroli <zack@debian.org>
6 Build-Depends: ocaml, ocaml-findlib, libgdome2-ocaml-dev, liblablgtk2-ocaml-dev, liblablgtkmathview-ocaml-dev, liblablgtksourceview-ocaml-dev, libsqlite3-ocaml-dev (>= 0.22.0), libocamlnet-ocaml-dev, libzip-ocaml-dev, libhttp-ocaml-dev, ocaml-ulex, libexpat-ocaml-dev, debhelper, cdbs, libmysql-ocaml-dev
7 Standards-Version: 3.7.2
8 XS-Vcs-Svn: svn://mowgli.cs.unibo.it/trunk/helm/software/pkg-matita/trunk/
9 XS-Vcs-Browser: http://helm.cs.unibo.it/websvn/listing.php?path=/trunk/helm/software/pkg-matita/trunk/
13 Depends: ${shlibs:Depends}
14 Recommends: matita-standard-library
15 Description: interactive theorem prover
16 Matita is a graphical interactive theorem prover based on the Calculus of
17 (Co)Inductive Constructions.
19 Matita adopts XML-encoded proof objects are produced for storage and exchange.
20 This makes it compatible, at some extent, with Coq.
22 The graphical interface has been inspired by CtCoq and Proof General. It
23 supports high quality bidimensional rendering of proofs and formulae
24 transformed on-the-fly to MathML markup
26 Package: matita-standard-library
29 Description: standard library for the Matita interactive theorem prover
30 Matita is a graphical interactive theorem prover based on the Calculus of
31 (Co)Inductive Constructions.
33 This package contains the standard library of theorems of the
34 matita interactive theorem prover.