--- a/NEWS Sun Apr 01 22:14:59 2012 +0200
+++ b/NEWS Sun Apr 01 22:41:56 2012 +0200
@@ -135,6 +135,10 @@
* Code generation by default implements sets as container type rather
than predicates. INCOMPATIBILITY.
+* New proof import from HOL Light, cf. HOL/Import. Requires a proof
+bundle, which is available as an external component. Removed old (and
+mostly dead) Importer for HOL4 and HOL Light. INCOMPATIBILITY.
+
* New type synonym 'a rel = ('a * 'a) set
* Theory Divides: Discontinued redundant theorems about div and mod.