--- a/src/HOL/List.thy Mon Sep 20 21:09:42 2010 +0200
+++ b/src/HOL/List.thy Tue Sep 21 02:03:40 2010 +0200
@@ -4206,6 +4206,9 @@
lemmas in_listsI [intro!,no_atp] = in_listspI [to_set]
+lemma lists_eq_set: "lists A = {xs. set xs <= A}"
+by auto
+
lemma lists_UNIV [simp]: "lists UNIV = UNIV"
by auto