src/HOL/Library/Quotient_List.thy

--- a/src/HOL/Library/Quotient_List.thy	Sat Apr 21 11:04:21 2012 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Sat Apr 21 11:21:23 2012 +0200
@@ -5,7 +5,7 @@
 header {* Quotient infrastructure for the list type *}
 
 theory Quotient_List
-imports Main Quotient_Syntax
+imports Main Quotient_Set
 begin
 
 subsection {* Relator for list type *}
@@ -157,6 +157,10 @@
   apply (simp, simp add: fun_rel_def)
   done
 
+lemma set_transfer [transfer_rule]:
+  "(list_all2 A ===> set_rel A) set set"
+  unfolding set_def by transfer_prover
+
 subsection {* Setup for lifting package *}
 
 lemma Quotient_list: