changeset 15426 | f41e3e654706 |
parent 15425 | 6356d2523f73 |
child 15439 | 71c0f98e31f1 |
--- a/src/HOL/List.thy Wed Dec 22 11:36:33 2004 +0100 +++ b/src/HOL/List.thy Tue Jan 04 04:06:29 2005 +0100 @@ -669,6 +669,10 @@ "list_all P (xs @ ys) = (list_all P xs \<and> list_all P ys)" by (induct xs) auto +lemma list_all_rev [simp]: "list_all P (rev xs) = list_all P xs" +by (simp add: list_all_conv) + + subsubsection {* @{text filter} *}