src/HOL/Library/Finite_Map.thy
changeset 64179 ce205d1f8592
parent 63900 2359e9952641
child 64180 676763a9c269
     1.1 --- a/src/HOL/Library/Finite_Map.thy	Wed Oct 12 21:48:53 2016 +0200
     1.2 +++ b/src/HOL/Library/Finite_Map.thy	Thu Oct 13 14:15:34 2016 +0200
     1.3 @@ -407,9 +407,6 @@
     1.4  lemma fmdrop_comm: "fmdrop a (fmdrop b m) = fmdrop b (fmdrop a m)"
     1.5  unfolding fmfilter_alt_defs by (rule fmfilter_comm)
     1.6  
     1.7 -lemma fmdrop_fmupd[simp]: "fmdrop x (fmupd x y m) = m"
     1.8 -oops
     1.9 -
    1.10  lift_definition fmadd :: "('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap" (infixl "++\<^sub>f" 100)
    1.11    is map_add
    1.12    parametric map_add_transfer