1.1 --- a/NEWS	Mon May 12 23:01:13 2008 +0200
     1.2 +++ b/NEWS	Tue May 13 09:10:56 2008 +0200
     1.3 @@ -244,6 +244,22 @@
     1.4  reconstruction_modulus, reconstruction_sorts renamed
     1.5  sledgehammer_modulus, sledgehammer_sorts.  INCOMPATIBILITY.
     1.6  
     1.7 +* More flexible generation of measure functions for termination proofs:
     1.8 +Measure functions can be declared by proving a rule of the form
     1.9 +"is_measure f" and giving it the [measure_function] attribute. The
    1.10 +"is_measure" predicate is logically meaningless (always true), and
    1.11 +just guides the heuristic.  To find suitable measure functions, the
    1.12 +termination prover sets up the goal "is_measure ?f" of the appropriate
    1.13 +type and generates all solutions by prolog-style backwards proof using
    1.14 +the declared rules.
    1.15 +
    1.16 +This setup also deals with rules like 
    1.17 +
    1.18 +  "is_measure f ==> is_measure (list_size f)"
    1.19 +
    1.20 +which accomodates nested datatypes that recurse through lists. Similar
    1.21 +rules are predeclared for products and option types.
    1.22 +
    1.23  
    1.24  *** ZF ***
    1.25