summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Number_Theory/UniqueFactorization.thy

changeset 36903 | 489c1fbbb028 |

parent 35644 | d20cf282342e |

child 37290 | 3464d7232670 |

--- a/src/HOL/Number_Theory/UniqueFactorization.thy Wed May 12 22:33:10 2010 -0700 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy Thu May 13 14:34:05 2010 +0200 @@ -56,11 +56,6 @@ apply auto done -(* Should this go in Multiset.thy? *) -(* TN: No longer an intro-rule; needed only once and might get in the way *) -lemma multiset_eqI: "[| !!x. count M x = count N x |] ==> M = N" - by (subst multiset_eq_conv_count_eq, blast) - (* Here is a version of set product for multisets. Is it worth moving to multiset.thy? If so, one should similarly define msetsum for abelian semirings, using of_nat. Also, is it worth developing bounded quantifiers @@ -210,7 +205,7 @@ ultimately have "count M a = count N a" by auto } - thus ?thesis by (simp add:multiset_eq_conv_count_eq) + thus ?thesis by (simp add:multiset_ext_iff) qed definition multiset_prime_factorization :: "nat => nat multiset" where