Bug#663754: ITP: hol-light -- HOL Light theorem prover

[Hendrik Tews <hendrik@askra.de>]

Package: wnpp
Owner: Hendrik Tews <hendrik@askra.de>
Severity: wishlist

* Package name    : hol-light
  Version         : 20120312
  Upstream Author : John Harrison
* URL or Web page : http://www.cl.cam.ac.uk/~jrh13/hol-light/
* License         : HOL Light licence
  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
 formalizing Tom Hales' proof of the Kepler conjecture. 


The upstream author very much appreciates this packaging
initiative. He is going to provide hints about which svn version
should be packaged (there are no normal releases of HOL Light).