src/HOL/List.thy

--- a/src/HOL/List.thy	Fri Apr 25 15:30:33 2008 +0200
+++ b/src/HOL/List.thy	Fri Apr 25 16:28:06 2008 +0200
@@ -3265,6 +3265,15 @@
 setup StringSyntax.setup
 
 
+subsection {* Size function *}
+
+declare [[measure_function "list_size size"]]
+
+lemma list_size_estimation[termination_simp]:
+  "x \<in> set xs \<Longrightarrow> f x < list_size f xs"
+by (induct xs) auto
+
+
 subsection {* Code generator *}
 
 subsubsection {* Setup *}