1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
Source: hol-light
Section: math
Priority: optional
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Uploaders:
Hendrik Tews <hendrik@askra.de>
Build-Depends:
debhelper-compat (= 12),
camlp5 (>= 7.11),
ocaml-base-nox,
libnum-ocaml-dev,
dh-ocaml
Standards-Version: 4.4.1
Rules-Requires-Root: no
Homepage: http://www.cl.cam.ac.uk/~jrh13/hol-light/
Vcs-Git: https://salsa.debian.org/ocaml-team/hol-light.git
Vcs-Browser: https://salsa.debian.org/ocaml-team/hol-light
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,
python
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.
|
