# HG changeset patch
# User bulwahn
# Date 1258013491 -3600
# Node ID ffb4a811e34d88af2a88c6dec8347ce987fad564
# Parent  42f69386943af24f46e0e67307dd2bd71db6be9d
announcing the predicate compiler in NEWS and CONTRIBUTORS

diff -r 42f69386943a -r ffb4a811e34d CONTRIBUTORS
--- a/CONTRIBUTORS	Thu Nov 12 09:11:26 2009 +0100
+++ b/CONTRIBUTORS	Thu Nov 12 09:11:31 2009 +0100
@@ -6,7 +6,9 @@
 
 Contributions to this Isabelle version
 --------------------------------------
-
+* November 2009: Lukas Bulwahn, TUM
+  Predicate Compiler: a compiler for inductive predicates to equational specfications
+ 
 * November 2009: Sascha Boehme, TUM
   HOL-Boogie: an interactive prover back-end for Boogie and VCC
 
diff -r 42f69386943a -r ffb4a811e34d NEWS
--- 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