NEWS
changeset 33627 ffb4a811e34d
parent 33524 a08e6c1cbc04
child 33639 603320b93668
--- a/NEWS	Thu Nov 12 09:11:26 2009 +0100
+++ b/NEWS	Thu Nov 12 09:11:31 2009 +0100
@@ -37,6 +37,9 @@
 
 *** HOL ***
 
+* New commands "code_pred" and "values" to invoke the predicate compiler
+and to enumerate values of inductive predicates.
+
 * Combined former theories Divides and IntDiv to one theory Divides
 in the spirit of other number theory theories in HOL;  some constants
 (and to a lesser extent also facts) have been suffixed with _nat und _int