# HG changeset patch
# User krauss
# Date 1230395701 -3600
# Node ID 9304afad825ef9ddc2b4ee5571aa708f5bac72e1
# Parent  cc177742e607de063c3b12875d17985e697c7b36
tuned NEWS; CONTRIBUTORS

diff -r cc177742e607 -r 9304afad825e CONTRIBUTORS
--- a/CONTRIBUTORS	Sat Dec 27 17:35:00 2008 +0100
+++ b/CONTRIBUTORS	Sat Dec 27 17:35:01 2008 +0100
@@ -7,6 +7,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* December 2008: Armin Heller, TUM and Alexander Krauss, TUM
+  Method "sizechange" for advanced termination proofs.
+
 * November 2008: Timothy Bourke, NICTA
   Performance improvement (factor 50) for find_theorems.
 
diff -r cc177742e607 -r 9304afad825e NEWS
--- a/NEWS	Sat Dec 27 17:35:00 2008 +0100
+++ b/NEWS	Sat Dec 27 17:35:01 2008 +0100
@@ -245,7 +245,8 @@
 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.
+modification of) the size-change principle. Requires SAT solver. See
+src/HOL/ex/Termination.thy for examples.
 
 * HOL/Orderings: class "wellorder" moved here, with explicit induction
 rule "less_induct" as assumption.  For instantiation of "wellorder" by