src/HOL/Library/Finite_Map.thy

--- a/src/HOL/Library/Finite_Map.thy	Wed Oct 12 21:48:53 2016 +0200
+++ b/src/HOL/Library/Finite_Map.thy	Thu Oct 13 14:15:34 2016 +0200
@@ -407,9 +407,6 @@
 lemma fmdrop_comm: "fmdrop a (fmdrop b m) = fmdrop b (fmdrop a m)"
 unfolding fmfilter_alt_defs by (rule fmfilter_comm)
 
-lemma fmdrop_fmupd[simp]: "fmdrop x (fmupd x y m) = m"
-oops
-
 lift_definition fmadd :: "('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap" (infixl "++\<^sub>f" 100)
   is map_add
   parametric map_add_transfer