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