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