# HG changeset patch
# User bulwahn
# Date 1369978223 -7200
# Node ID 86d6f57c2c1e28d04ad736122740936e8159ca0d
# Parent  bb907eba5902ddf79e1458edc665371409084c46
NEWS about Spec_Check

diff -r bb907eba5902 -r 86d6f57c2c1e CONTRIBUTORS
--- a/CONTRIBUTORS	Thu May 30 23:29:33 2013 +0200
+++ b/CONTRIBUTORS	Fri May 31 07:30:23 2013 +0200
@@ -6,6 +6,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* May 2013: Lukas Bulwahn and Nicolai Schaffroth, TUM
+  HOL-Spec_Check: A Quickcheck tool for Isabelle's ML environment.
+
 * April 2013: Stefan Berghofer, secunet Security Networks AG
   Dmitriy Traytel, TUM
   Makarius Wenzel, Université Paris-Sud / LRI
diff -r bb907eba5902 -r 86d6f57c2c1e NEWS
--- a/NEWS	Thu May 30 23:29:33 2013 +0200
+++ b/NEWS	Fri May 31 07:30:23 2013 +0200
@@ -210,6 +210,13 @@
   - Renamed option:
       isar_shrink ~> isar_compress
 
+* HOL-Spec_Check: a Quickcheck tool for Isabelle's ML environment.
+  
+  With HOL-Spec_Check, ML developers can check specifications with the
+  ML function check_property. The specifications must be of the form
+  "ALL x1 ... xn. Prop x1 ... xn". Simple examples are in
+  src/HOL/Spec_Check/Examples.thy.
+
 
 *** HOL-Algebra ***