remove accidentally oops'ed (and wrong) lemma
authorLars Hupel <lars.hupel@mytum.de>
Thu, 13 Oct 2016 14:15:34 +0200
changeset 64179 ce205d1f8592
parent 64178 12e6c3bbb488
child 64180 676763a9c269
remove accidentally oops'ed (and wrong) lemma
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