# HG changeset patch
# User kleing
# Date 1104807989 -3600
# Node ID f41e3e6547060f00325480e5024b2dae4ff3cb5a
# Parent  6356d2523f73d0271e131a2e794eeb7379a52f27
added list_all_rev

diff -r 6356d2523f73 -r f41e3e654706 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} *}