# HG changeset patch
# User berghofe
# Date 1295092150 -3600
# Node ID 72dd2eec64d88e03aa6b71b1e96f25c7f54c882f
# Parent  676b32bea254df4740d99b67d5d6fb33877d3124
Added entry for HOL-SPARK

diff -r 676b32bea254 -r 72dd2eec64d8 CONTRIBUTORS
--- 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.
 
diff -r 676b32bea254 -r 72dd2eec64d8 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 ***