src/HOL/List.thy

--- 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} *}