Added entry for HOL-SPARK
authorberghofe
Sat Jan 15 12:49:10 2011 +0100 (2011-01-15)
changeset 4156772dd2eec64d8
parent 41566 676b32bea254
child 41568 a6304284b5ef
Added entry for HOL-SPARK
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Sat Jan 15 12:48:39 2011 +0100
     1.2 +++ b/CONTRIBUTORS	Sat Jan 15 12:49:10 2011 +0100
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to Isabelle2011
     1.5  -----------------------------
     1.6  
     1.7 +* January 2011: Stefan Berghofer, secunet Security Networks AG
     1.8 +  HOL-SPARK: an interactive prover back-end for SPARK.
     1.9 +
    1.10  * October 2010: Bogdan Grechuk, University of Edinburgh
    1.11    Extended convex analysis in Multivariate Analysis.
    1.12  
     2.1 --- a/NEWS	Sat Jan 15 12:48:39 2011 +0100
     2.2 +++ b/NEWS	Sat Jan 15 12:49:10 2011 +0100
     2.3 @@ -510,6 +510,9 @@
     2.4  * Removed lemma Option.is_none_none (Duplicate of is_none_def).
     2.5  INCOMPATIBILITY.
     2.6  
     2.7 +* New commands to load and prove verification conditions generated by
     2.8 +the SPARK Ada program verifier.  See src/HOL/SPARK.
     2.9 +
    2.10  
    2.11  *** HOL-Algebra ***
    2.12