# HG changeset patch
# User nipkow
# Date 1285027420 -7200
# Node ID 48f63a6c7f851f283eb90887a615acb5b46565b6
# Parent  61018b8d3e49b402e5a069ffbddbeef0f2e15278
new lemma

diff -r 61018b8d3e49 -r 48f63a6c7f85 src/HOL/List.thy
--- 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