NEWS about Spec_Check
authorbulwahn
Fri May 31 07:30:23 2013 +0200 (2013-05-31 ago)
changeset 5226686d6f57c2c1e
parent 52265 bb907eba5902
child 52270 19bd34e97e2e
NEWS about Spec_Check
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Thu May 30 23:29:33 2013 +0200
     1.2 +++ b/CONTRIBUTORS	Fri May 31 07:30:23 2013 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* May 2013: Lukas Bulwahn and Nicolai Schaffroth, TUM
     1.8 +  HOL-Spec_Check: A Quickcheck tool for Isabelle's ML environment.
     1.9 +
    1.10  * April 2013: Stefan Berghofer, secunet Security Networks AG
    1.11    Dmitriy Traytel, TUM
    1.12    Makarius Wenzel, Université Paris-Sud / LRI
     2.1 --- a/NEWS	Thu May 30 23:29:33 2013 +0200
     2.2 +++ b/NEWS	Fri May 31 07:30:23 2013 +0200
     2.3 @@ -210,6 +210,13 @@
     2.4    - Renamed option:
     2.5        isar_shrink ~> isar_compress
     2.6  
     2.7 +* HOL-Spec_Check: a Quickcheck tool for Isabelle's ML environment.
     2.8 +  
     2.9 +  With HOL-Spec_Check, ML developers can check specifications with the
    2.10 +  ML function check_property. The specifications must be of the form
    2.11 +  "ALL x1 ... xn. Prop x1 ... xn". Simple examples are in
    2.12 +  src/HOL/Spec_Check/Examples.thy.
    2.13 +
    2.14  
    2.15  *** HOL-Algebra ***
    2.16