NEWS

--- a/NEWS	Mon Aug 31 20:34:44 2009 +0200
+++ b/NEWS	Mon Aug 31 20:34:48 2009 +0200
@@ -112,6 +112,9 @@
 Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
 Suc_plus1 -> Suc_eq_plus1
 
+* Moved theorems:
+Wellfounded.in_inv_image -> Relation.in_inv_image
+
 * New sledgehammer option "Full Types" in Proof General settings menu.
 Causes full type information to be output to the ATPs.  This slows
 ATPs down considerably but eliminates a source of unsound "proofs"