src/HOL/Number_Theory/UniqueFactorization.thy
changeset 33657 a4179bf442d1
parent 32479 521cc9bf2958
child 34947 e1b8f2736404
--- 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