# HG changeset patch
# User nipkow
# Date 1369979740 -7200
# Node ID 19bd34e97e2e826f85ca113de1e35d3423c23848
# Parent  86d6f57c2c1e28d04ad736122740936e8159ca0d# Parent  d867812da48b10b88db52d0ffc67f43bcd6e58d3
merged

diff -r d867812da48b -r 19bd34e97e2e CONTRIBUTORS
--- a/CONTRIBUTORS	Fri May 31 07:55:09 2013 +0200
+++ b/CONTRIBUTORS	Fri May 31 07:55:40 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 d867812da48b -r 19bd34e97e2e NEWS
--- a/NEWS	Fri May 31 07:55:09 2013 +0200
+++ b/NEWS	Fri May 31 07:55:40 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 ***