# HG changeset patch
# User huffman
# Date 1337009287 -7200
# Node ID ba9df9685e7c2d59ebd40836fc41e89748c6ddc2
# Parent  bba52dffab2bd165b1e68726d1c0c5ceee27b0cf
add transfer rule for constant List.lists

diff -r bba52dffab2b -r ba9df9685e7c src/HOL/Library/Quotient_List.thy
--- 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]: