# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1476360934 -7200
# Node ID ce205d1f8592da53253b7d088ca27419fcfa21b1
# Parent  12e6c3bbb488499f5183de57b48c80e07eaf3596
remove accidentally oops'ed (and wrong) lemma

diff -r 12e6c3bbb488 -r ce205d1f8592 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