added auto_quickcheck feature;
authorwenzelm
Mon Oct 01 21:19:52 2007 +0200 (2007-10-01)
changeset 24804513bb015b469
parent 24803 38577b4b1fde
child 24805 34cbfb87dfe8
added auto_quickcheck feature;
NEWS
     1.1 --- a/NEWS	Mon Oct 01 21:19:50 2007 +0200
     1.2 +++ b/NEWS	Mon Oct 01 21:19:52 2007 +0200
     1.3 @@ -529,6 +529,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* New "auto_quickcheck" feature tests outermost goal statements for
     1.8 +potential counter-examples.  Controlled by ML references
     1.9 +auto_quickcheck (default true) and auto_quickcheck_time_limit (default
    1.10 +5000 milliseconds).
    1.11 +
    1.12  * Internal reorganisation of `size' of datatypes: size theorems
    1.13  "foo.size" are no longer subsumed by "foo.simps" (but are still
    1.14  simplification rules by default!); theorems "prod.size" now named