# HG changeset patch
# User krauss
# Date 1210662656 -7200
# Node ID c3bb1f39781125c4c3c58585d6dffdbda279f038
# Parent  d50ef6b952ba64dc68b0a2534c3cf4844ce550db
NEWS about measure functions

diff -r d50ef6b952ba -r c3bb1f397811 NEWS
--- a/NEWS	Mon May 12 23:01:13 2008 +0200
+++ b/NEWS	Tue May 13 09:10:56 2008 +0200
@@ -244,6 +244,22 @@
 reconstruction_modulus, reconstruction_sorts renamed
 sledgehammer_modulus, sledgehammer_sorts.  INCOMPATIBILITY.
 
+* More flexible generation of measure functions for termination proofs:
+Measure functions can be declared by proving a rule of the form
+"is_measure f" and giving it the [measure_function] attribute. The
+"is_measure" predicate is logically meaningless (always true), and
+just guides the heuristic.  To find suitable measure functions, the
+termination prover sets up the goal "is_measure ?f" of the appropriate
+type and generates all solutions by prolog-style backwards proof using
+the declared rules.
+
+This setup also deals with rules like 
+
+  "is_measure f ==> is_measure (list_size f)"
+
+which accomodates nested datatypes that recurse through lists. Similar
+rules are predeclared for products and option types.
+
 
 *** ZF ***