changeset 61565 | 352c73a689da |
parent 61343 | 5b5656a63bd6 |
child 61566 | c3d6e570ccef |
--- a/src/HOL/ex/LocaleTest2.thy Tue Nov 03 18:11:59 2015 +0100 +++ b/src/HOL/ex/LocaleTest2.thy Wed Nov 04 08:13:49 2015 +0100 @@ -826,7 +826,7 @@ proof - have "hom one +++ zero = hom one +++ hom one" by (simp add: hom_mult [symmetric] del: hom_mult) - then show ?thesis by (simp del: r_one) + then show ?thesis by (simp del: sum.r_one) qed end