changeset 21240 8e75fb38522c
parent 21226 a607ae87ee81
child 21241 a00a16cbc647
--- a/NEWS	Wed Nov 08 02:13:02 2006 +0100
+++ b/NEWS	Wed Nov 08 09:08:54 2006 +0100
@@ -476,6 +476,22 @@
 *** HOL ***
+* Automated termination proofs "by lexicographic_order" are now
+included in the abbreviated function command "fun". No explicit
+"termination" command is necessary anymore.
+INCOMPATIBILITY: If a "fun"-definition cannot be proved terminating by
+a lexicographic size order, then the command fails. Use the expanded
+version "function" for these cases.
+* New method "lexicographic_order" automatically synthesizes
+termination relations as lexicographic combinations of size measures. 
+Usage for (function package) termination proofs:
+by lexicographic_order
+Contributed by Lukas Bulwahn.
 * Records: generalised field-update to take a function on the field 
 rather than the new value: r(|A := x|) is translated to A_update (K x) r
 The K-combinator that is internally used is called K_record.