Package: wnpp Owner: Hendrik Tews <hend...@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). -- To UNSUBSCRIBE, email to debian-wnpp-requ...@lists.debian.org with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org Archive: http://lists.debian.org/87pqcg44ot....@wallace.tews.net