Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
strengthening list_size_pointwise (thanks to Rene Thiemann)
authorbulwahn
Tue, 30 Aug 2011 20:10:47 +0200
changeset 44618 f3635643a376
parent 44604 1ad3159323dc
child 44619 fd520fa2fb09
strengthening list_size_pointwise (thanks to Rene Thiemann)
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- 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+
isabelle