# HG changeset patch
# User krauss
# Date 1233656188 -3600
# Node ID 2786b348c376d0c88e6de889827f49cbcf0df68c
# Parent  b5156537067ddfabc28c347225ebe07757a434c4
declare "nat o abs" as default measure for int

diff -r b5156537067d -r 2786b348c376 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*}