NEWS

--- a/NEWS	Sat Jan 15 12:48:39 2011 +0100
+++ b/NEWS	Sat Jan 15 12:49:10 2011 +0100
@@ -510,6 +510,9 @@
 * Removed lemma Option.is_none_none (Duplicate of is_none_def).
 INCOMPATIBILITY.
 
+* New commands to load and prove verification conditions generated by
+the SPARK Ada program verifier.  See src/HOL/SPARK.
+
 
 *** HOL-Algebra ***