# HG changeset patch
# User nipkow
# Date 1636529810 -3600
# Node ID ed1e5ea253698d19f3cba3fc20f4c7dc65a707fa
# Parent  5ae76214565ff037e5257bf47d75a7e1cb4721b3
added lemma

diff -r 5ae76214565f -r ed1e5ea25369 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Nov 09 19:47:24 2021 +0100
+++ b/src/HOL/List.thy	Wed Nov 10 08:36:50 2021 +0100
@@ -1545,6 +1545,8 @@
 lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)"
 by (induct xs) simp_all
 
+lemmas empty_filter_conv = filter_empty_conv[THEN eq_iff_swap]
+
 lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)"
 proof (induct xs)
   case (Cons x xs)