--- a/src/HOL/Library/Multiset.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Sep 12 07:55:43 2011 +0200
@@ -218,7 +218,7 @@
lemma add_eq_conv_diff:
"M + {#a#} = N + {#b#} \<longleftrightarrow> M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#}" (is "?lhs = ?rhs")
-(* shorter: by (simp add: multiset_eq_iff) fastsimp *)
+(* shorter: by (simp add: multiset_eq_iff) fastforce *)
proof
assume ?rhs then show ?lhs
by (auto simp add: add_assoc add_commute [of "{#b#}"])