NEWS
changeset 29182 9304afad825e
parent 29162 bad036eb71c4
child 29197 6d4cb27ed19c
--- 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