# HG changeset patch
# User kuncar
# Date 1368612644 -7200
# Node ID 07344a4f19db574726851fc55830927b6661c3dd
# Parent  82cc2aeb7d1392d53ab4515ef282af794b8f728f
superfluous transfer rule

diff -r 82cc2aeb7d13 -r 07344a4f19db src/HOL/Library/FinFun.thy
--- a/src/HOL/Library/FinFun.thy	Wed May 15 12:10:39 2013 +0200
+++ b/src/HOL/Library/FinFun.thy	Wed May 15 12:10:44 2013 +0200
@@ -420,10 +420,6 @@
 lift_definition finfun_default :: "'a \<Rightarrow>f 'b \<Rightarrow> 'b"
 is "finfun_default_aux" ..
 
-lemma finfun_apply_transfer [transfer_rule]: 
-  "(fun_rel cr_finfun (fun_rel op = op =)) (\<lambda>f. f) finfun_apply"
-unfolding Rel_def fun_rel_def cr_finfun_def by simp
-
 lemma finite_finfun_default: "finite {a. finfun_apply f a \<noteq> finfun_default f}"
 by transfer (erule finite_finfun_default_aux)