author | Lars Hupel <lars.hupel@mytum.de> |
Thu, 13 Oct 2016 14:15:34 +0200 | |
changeset 64179 | ce205d1f8592 |
parent 64178 | 12e6c3bbb488 |
child 64180 | 676763a9c269 |
--- 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