--- a/CONTRIBUTORS Sat Jan 15 12:48:39 2011 +0100
+++ b/CONTRIBUTORS Sat Jan 15 12:49:10 2011 +0100
@@ -6,6 +6,9 @@
Contributions to Isabelle2011
-----------------------------
+* January 2011: Stefan Berghofer, secunet Security Networks AG
+ HOL-SPARK: an interactive prover back-end for SPARK.
+
* October 2010: Bogdan Grechuk, University of Edinburgh
Extended convex analysis in Multivariate Analysis.
--- 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 ***