announcing the predicate compiler in NEWS and CONTRIBUTORS
authorbulwahn
Thu Nov 12 09:11:31 2009 +0100 (2009-11-12)
changeset 33627ffb4a811e34d
parent 33626 42f69386943a
child 33628 ed2111a5c3ed
announcing the predicate compiler in NEWS and CONTRIBUTORS
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Thu Nov 12 09:11:26 2009 +0100
     1.2 +++ b/CONTRIBUTORS	Thu Nov 12 09:11:31 2009 +0100
     1.3 @@ -6,7 +6,9 @@
     1.4  
     1.5  Contributions to this Isabelle version
     1.6  --------------------------------------
     1.7 -
     1.8 +* November 2009: Lukas Bulwahn, TUM
     1.9 +  Predicate Compiler: a compiler for inductive predicates to equational specfications
    1.10 + 
    1.11  * November 2009: Sascha Boehme, TUM
    1.12    HOL-Boogie: an interactive prover back-end for Boogie and VCC
    1.13  
     2.1 --- a/NEWS	Thu Nov 12 09:11:26 2009 +0100
     2.2 +++ b/NEWS	Thu Nov 12 09:11:31 2009 +0100
     2.3 @@ -37,6 +37,9 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 +* New commands "code_pred" and "values" to invoke the predicate compiler
     2.8 +and to enumerate values of inductive predicates.
     2.9 +
    2.10  * Combined former theories Divides and IntDiv to one theory Divides
    2.11  in the spirit of other number theory theories in HOL;  some constants
    2.12  (and to a lesser extent also facts) have been suffixed with _nat und _int