Package: hol-light Version: 20120602-1 Severity: minor Tags: patch Dear Hendrik,
I found a small typo in the package description of hol-light while translating it via the DDTSS. It says "as well as for the Flyspec project", but the project is called Flyspeck[2]. A patch for the control file is included. Regards, Erik [1] http://ddtp.debian.net/ddtss/index.cgi/xx [2] https://code.google.com/p/flyspeck/
--- control 2012-06-12 07:34:41.000000000 +0200 +++ control.new 2012-07-06 12:57:13.267719215 +0200 @@ -33,5 +33,5 @@ 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 + arithmetic as well as for the Flyspeck project, which aims at the formalization of Tom Hales' proof of the Kepler conjecture.
