# HG changeset patch
# User huffman
# Date 1334999061 -7200
# Node ID df687f0797fb7fd01d2d4557a045a274a76bf029
# Parent  6b9d20a095ae6906b4a38cfb148ed77d79621280
remove duplicate of lemma id_transfer

diff -r 6b9d20a095ae -r df687f0797fb src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Sat Apr 21 11:02:01 2012 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Sat Apr 21 11:04:21 2012 +0200
@@ -120,9 +120,6 @@
   "((A ===> op =) ===> list_all2 A ===> list_all2 A) filter filter"
   unfolding List.filter_def by transfer_prover
 
-lemma id_transfer [transfer_rule]: "(A ===> A) id id"
-  unfolding fun_rel_def by simp
-
 lemma foldr_transfer [transfer_rule]:
   "((A ===> B ===> B) ===> list_all2 A ===> B ===> B) foldr foldr"
   unfolding List.foldr_def by transfer_prover