1.1 --- a/CONTRIBUTORS	Sat Dec 27 17:35:00 2008 +0100
     1.2 +++ b/CONTRIBUTORS	Sat Dec 27 17:35:01 2008 +0100
     1.3 @@ -7,6 +7,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* December 2008: Armin Heller, TUM and Alexander Krauss, TUM
     1.8 +  Method "sizechange" for advanced termination proofs.
     1.9 +
    1.10  * November 2008: Timothy Bourke, NICTA
    1.11    Performance improvement (factor 50) for find_theorems.
    1.12  

     2.1 --- a/NEWS	Sat Dec 27 17:35:00 2008 +0100
     2.2 +++ b/NEWS	Sat Dec 27 17:35:01 2008 +0100
     2.3 @@ -245,7 +245,8 @@
     2.4  further src/HOL/ex/Eval_Examples.thy.
     2.5  
     2.6  * New method "sizechange" to automate termination proofs using (a
     2.7 -modification of) the size-change principle. Requires SAT solver.
     2.8 +modification of) the size-change principle. Requires SAT solver. See
     2.9 +src/HOL/ex/Termination.thy for examples.
    2.10  
    2.11  * HOL/Orderings: class "wellorder" moved here, with explicit induction
    2.12  rule "less_induct" as assumption.  For instantiation of "wellorder" by