Package: hol-light
Version: 1:3.1.0-2build3
Architecture: amd64
Architecture-Variant: amd64v3
Maintainer: Ubuntu Developers <ubuntu-devel-discuss@lists.ubuntu.com>
Original-Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Installed-Size: 47607
Depends: camlp5, camlp5-r35f8, libcamlp-streams-ocaml-dev-hv4j2, libcompiler-libs-ocaml-dev-dv595, libpcre2-ocaml-dev-13mc2, libstdlib-ocaml-dev-kjuo1, libzarith-ocaml-dev-0x2c5, ocaml-5.4.0
Suggests: readline-editor, prover9, coinor-csdp, pari-gp, maxima, dmtcp, libocamlgraph-ocaml-dev, python
Section: math
Priority: optional
Homepage: https://www.cl.cam.ac.uk/~jrh13/hol-light/
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 aimed at the
 formalization of Tom Hales' proof of the Kepler conjecture.
