Added two paragraphs on "rules" method and code generator.
authorberghofe
Tue Mar 05 18:54:55 2002 +0100 (2002-03-05)
changeset 13023f869b6822006
parent 13022 b115b305612f
child 13024 0461b281c2b5
Added two paragraphs on "rules" method and code generator.
NEWS
     1.1 --- a/NEWS	Tue Mar 05 18:19:11 2002 +0100
     1.2 +++ b/NEWS	Tue Mar 05 18:54:55 2002 +0100
     1.3 @@ -151,6 +151,10 @@
     1.4  text; the fixed correlation with particular command syntax has been
     1.5  discontinued;
     1.6  
     1.7 +* Pure: new method 'rules' is particularly well-suited for proof
     1.8 +search in intuitionistic logic; a bit slower than 'blast' or 'fast',
     1.9 +but often produces more compact proof terms with less detours;
    1.10 +
    1.11  * Pure/Provers/classical: simplified integration with pure rule
    1.12  attributes and methods; the classical "intro?/elim?/dest?"
    1.13  declarations coincide with the pure ones; the "rule" method no longer
    1.14 @@ -233,6 +237,11 @@
    1.15    - internal definitions directly based on a light-weight abstract
    1.16      theory of product types over typedef rather than datatype;
    1.17  
    1.18 +* HOL: generic code generator for generating executable ML code from
    1.19 +specifications; specific support for HOL constructs such as inductive
    1.20 +datatypes and sets, as well as recursive functions; can be invoked
    1.21 +via 'generate_code' theory section;
    1.22 +
    1.23  * HOL: canonical cases/induct rules for n-tuples (n = 3..7);
    1.24  
    1.25  * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"