changeset 41567 | 72dd2eec64d8 |
parent 41512 | 8445396e1e39 |
child 41572 | 089049b768c6 |
--- 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 ***