src/HOL/Int.thy

--- a/src/HOL/Int.thy	Tue Feb 03 07:44:10 2009 +0100
+++ b/src/HOL/Int.thy	Tue Feb 03 11:16:28 2009 +0100
@@ -478,6 +478,9 @@
 
 end
 
+text {* For termination proofs: *}
+lemma measure_function_int[measure_function]: "is_measure (nat o abs)" ..
+
 
 subsection{*Lemmas about the Function @{term of_nat} and Orderings*}