# HG changeset patch
# User huffman
# Date 1335000083 -7200
# Node ID 33ecf14d5ee9fbe6c07291ea439119c5c5ff83ad
# Parent  df687f0797fb7fd01d2d4557a045a274a76bf029
add transfer rule for List.set

diff -r df687f0797fb -r 33ecf14d5ee9 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: