--- a/NEWS Tue Dec 16 00:19:47 2008 +0100
+++ b/NEWS Tue Dec 16 08:46:07 2008 +0100
@@ -239,6 +239,9 @@
mechanisms may be specified (currently, [SML], [code] or [nbe]). See
further src/HOL/ex/Eval_Examples.thy.
+* New method "sizechange" to automate termination proofs using (a
+modification of) the size-change principle. Requires SAT solver.
+
* HOL/Orderings: class "wellorder" moved here, with explicit induction
rule "less_induct" as assumption. For instantiation of "wellorder" by
means of predicate "wf", use rule wf_wellorderI. INCOMPATIBILITY.