Source: hol-light
Section: math
Priority: extra
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Uploaders:
 Hendrik Tews <hendrik@askra.de>
Build-Depends: 
 camlp5 (>= 6.0.7),
 ocaml-base-nox,
 dh-ocaml (>= 0.9~),
 debhelper (>= 9.0.0)
Standards-Version: 3.9.8
Homepage: http://www.cl.cam.ac.uk/~jrh13/hol-light/
Vcs-Git: https://anonscm.debian.org/cgit/pkg-ocaml-maint/packages/hol-light.git
Vcs-Browser: https://anonscm.debian.org/gitweb/?p=pkg-ocaml-maint/packages/hol-light.git

Package: hol-light
Architecture: any
Depends:
 camlp5,
 ${ocaml:Depends},
 ${shlibs:Depends}, 
 ${misc:Depends}
Suggests:
 readline-editor,
 prover9,
 coinor-csdp,
 pari-gp,
 maxima,
 dmtcp,
 libocamlgraph-ocaml-dev
Description: HOL Light theorem prover
 HOL Light is an interactive theorem prover for Higher-Order Logic
 with a very simple logical core running in an OCaml toplevel. HOL
 Light is famous for the verification of floating-point
 arithmetic as well as for the Flyspeck project, which aims at the
 formalization of Tom Hales' proof of the Kepler conjecture.