src/HOL/Library/Multiset.thy
changeset 44890 22f665a2e91c
parent 44339 eda6aef75939
child 45608 13b101cee425
     1.1 --- a/src/HOL/Library/Multiset.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -218,7 +218,7 @@
     1.4  
     1.5  lemma add_eq_conv_diff:
     1.6    "M + {#a#} = N + {#b#} \<longleftrightarrow> M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#}"  (is "?lhs = ?rhs")
     1.7 -(* shorter: by (simp add: multiset_eq_iff) fastsimp *)
     1.8 +(* shorter: by (simp add: multiset_eq_iff) fastforce *)
     1.9  proof
    1.10    assume ?rhs then show ?lhs
    1.11    by (auto simp add: add_assoc add_commute [of "{#b#}"])