src/HOL/List.thy
changeset 44618 f3635643a376
parent 44510 5e580115dfcd
child 44619 fd520fa2fb09
     1.1 --- a/src/HOL/List.thy	Tue Aug 30 17:53:03 2011 +0200
     1.2 +++ b/src/HOL/List.thy	Tue Aug 30 20:10:47 2011 +0200
     1.3 @@ -4907,7 +4907,7 @@
     1.4  by (induct xs) auto
     1.5  
     1.6  lemma list_size_pointwise[termination_simp]: 
     1.7 -  "(\<And>x. x \<in> set xs \<Longrightarrow> f x < g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
     1.8 +  "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
     1.9  by (induct xs) force+
    1.10  
    1.11