# HG changeset patch
# User bulwahn
# Date 1314727847 -7200
# Node ID f3635643a376b7b3038fecce0de5eaa2934ac617
# Parent  1ad3159323dc816b282781a6dd57cb23314f0bb9
strengthening list_size_pointwise (thanks to Rene Thiemann)

diff -r 1ad3159323dc -r f3635643a376 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Aug 30 17:53:03 2011 +0200
+++ b/src/HOL/List.thy	Tue Aug 30 20:10:47 2011 +0200
@@ -4907,7 +4907,7 @@
 by (induct xs) auto
 
 lemma list_size_pointwise[termination_simp]: 
-  "(\<And>x. x \<in> set xs \<Longrightarrow> f x < g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
+  "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
 by (induct xs) force+