--- 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.
--- 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