--- 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
--- 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 ***