--- a/src/HOL/Number_Theory/UniqueFactorization.thy Fri Feb 26 22:15:09 2016 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Fri Feb 26 22:44:11 2016 +0100
@@ -93,7 +93,7 @@
next
case False
then show ?thesis
- by auto
+ by (auto simp add: not_in_iff)
qed
finally have "a ^ count M a dvd a ^ count N a * (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)" .
moreover
@@ -111,7 +111,7 @@
next
case False
then show ?thesis
- by auto
+ by (auto simp add: not_in_iff)
qed
lemma multiset_prime_factorization_unique:
@@ -437,7 +437,7 @@
apply (cases "n = 0")
apply auto
apply (frule multiset_prime_factorization)
- apply (auto simp add: set_mset_def multiplicity_nat_def)
+ apply (auto simp add: multiplicity_nat_def count_eq_zero_iff)
done
lemma multiplicity_not_factor_nat [simp]: