changeset 13023 f869b6822006
parent 12984 6071200efbf6
child 13025 433c57d09d53
--- a/NEWS	Tue Mar 05 18:19:11 2002 +0100
+++ b/NEWS	Tue Mar 05 18:54:55 2002 +0100
@@ -151,6 +151,10 @@
 text; the fixed correlation with particular command syntax has been
+* Pure: new method 'rules' is particularly well-suited for proof
+search in intuitionistic logic; a bit slower than 'blast' or 'fast',
+but often produces more compact proof terms with less detours;
 * Pure/Provers/classical: simplified integration with pure rule
 attributes and methods; the classical "intro?/elim?/dest?"
 declarations coincide with the pure ones; the "rule" method no longer
@@ -233,6 +237,11 @@
   - internal definitions directly based on a light-weight abstract
     theory of product types over typedef rather than datatype;
+* HOL: generic code generator for generating executable ML code from
+specifications; specific support for HOL constructs such as inductive
+datatypes and sets, as well as recursive functions; can be invoked
+via 'generate_code' theory section;
 * HOL: canonical cases/induct rules for n-tuples (n = 3..7);
 * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"