deb_control_files:
- control
- md5sums
- postinst
- postrm
deb_fields:
Architecture: arm64
Depends: camlp5, camlp5-ui6s9, libcamlp-streams-ocaml-dev-764l3, libcompiler-libs-ocaml-dev-lw6m5,
libstdlib-ocaml-dev-0d647, libzarith-ocaml-dev-mtsj7, ocaml-5.2.0
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.
Homepage: https://www.cl.cam.ac.uk/~jrh13/hol-light/
Installed-Size: '45968'
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Package: hol-light
Priority: optional
Section: math
Suggests: readline-editor, prover9, coinor-csdp, pari-gp, maxima, dmtcp, libocamlgraph-ocaml-dev,
python
Version: 1:3.0.0-2
srcpkg_name: hol-light
srcpkg_version: 1:3.0.0-2