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