--- a/src/HOL/Number_Theory/UniqueFactorization.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Fri Nov 13 14:14:04 2009 +0100
@@ -844,7 +844,7 @@
mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
shows "x = y"
- apply (rule dvd_anti_sym)
+ apply (rule dvd_antisym)
apply (auto intro: multiplicity_dvd'_nat)
done
@@ -854,7 +854,7 @@
mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
shows "x = y"
- apply (rule dvd_anti_sym [transferred])
+ apply (rule dvd_antisym [transferred])
apply (auto intro: multiplicity_dvd'_int)
done