remove duplicate of lemma id_transfer
authorhuffman
Sat Apr 21 11:04:21 2012 +0200 (2012-04-21)
changeset 47649df687f0797fb
parent 47648 6b9d20a095ae
child 47650 33ecf14d5ee9
remove duplicate of lemma id_transfer
src/HOL/Library/Quotient_List.thy
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Sat Apr 21 11:02:01 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Sat Apr 21 11:04:21 2012 +0200
     1.3 @@ -120,9 +120,6 @@
     1.4    "((A ===> op =) ===> list_all2 A ===> list_all2 A) filter filter"
     1.5    unfolding List.filter_def by transfer_prover
     1.6  
     1.7 -lemma id_transfer [transfer_rule]: "(A ===> A) id id"
     1.8 -  unfolding fun_rel_def by simp
     1.9 -
    1.10  lemma foldr_transfer [transfer_rule]:
    1.11    "((A ===> B ===> B) ===> list_all2 A ===> B ===> B) foldr foldr"
    1.12    unfolding List.foldr_def by transfer_prover