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
|
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:
camlp5 (>= 6.0.4),
ocaml-base-nox,
dh-ocaml (>= 0.9~),
debhelper (>= 9.0.0)
Standards-Version: 3.9.3
Homepage: http://www.cl.cam.ac.uk/~jrh13/hol-light/
Vcs-Git: git://git.debian.org/git/pkg-ocaml-maint/packages/hol-light.git
Vcs-Browser: http://git.debian.org/?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 Flyspec project, which aims at the
formalization of Tom Hales' proof of the Kepler conjecture.
|
