--- a/src/HOL/Library/Quotient_List.thy Mon May 14 17:09:11 2012 +0200
+++ b/src/HOL/Library/Quotient_List.thy Mon May 14 17:28:07 2012 +0200
@@ -176,6 +176,15 @@
"(list_all2 A ===> set_rel A) set set"
unfolding set_def by transfer_prover
+lemma lists_transfer [transfer_rule]:
+ "(set_rel A ===> set_rel (list_all2 A)) lists lists"
+ apply (rule fun_relI, rule set_relI)
+ apply (erule lists.induct, simp)
+ apply (simp only: set_rel_def list_all2_Cons1, metis lists.Cons)
+ apply (erule lists.induct, simp)
+ apply (simp only: set_rel_def list_all2_Cons2, metis lists.Cons)
+ done
+
subsection {* Setup for lifting package *}
lemma Quotient_list[quot_map]: