| changeset 41550 | efa734d9b221 |
| parent 41229 | d797baa3d57c |
| child 42163 | 392fd6c4669c |
--- a/src/HOL/Map.thy Fri Jan 14 15:43:04 2011 +0100 +++ b/src/HOL/Map.thy Fri Jan 14 15:44:47 2011 +0100 @@ -111,7 +111,7 @@ assumes "m(a\<mapsto>x) = n(a\<mapsto>y)" shows "x = y" proof - - from prems have "(m(a\<mapsto>x)) a = (n(a\<mapsto>y)) a" by simp + from assms have "(m(a\<mapsto>x)) a = (n(a\<mapsto>y)) a" by simp then show ?thesis by simp qed