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