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