diff -r 8aab63a91053 -r 0a0d6d79d984 doc-src/TutorialI/Rules/Primes.thy
--- a/doc-src/TutorialI/Rules/Primes.thy	Wed Nov 18 14:00:08 2009 +0100
+++ b/doc-src/TutorialI/Rules/Primes.thy	Thu Nov 19 08:19:57 2009 +0100
@@ -112,13 +112,13 @@
 (*uniqueness of GCDs*)
 lemma is_gcd_unique: "\<lbrakk> is_gcd m a b; is_gcd n a b \<rbrakk> \<Longrightarrow> m=n"
 apply (simp add: is_gcd_def);
-apply (blast intro: dvd_anti_sym)
+apply (blast intro: dvd_antisym)
 done
 
 
 text {*
-@{thm[display] dvd_anti_sym}
-\rulename{dvd_anti_sym}
+@{thm[display] dvd_antisym}
+\rulename{dvd_antisym}
 
 \begin{isabelle}
 proof\ (prove):\ step\ 1\isanewline
@@ -154,7 +154,7 @@
   apply (auto intro: dvd_trans [of _ m])
   done
 
-(*This is half of the proof (by dvd_anti_sym) of*)
+(*This is half of the proof (by dvd_antisym) of*)
 lemma gcd_mult_cancel: "gcd k n = 1 \<Longrightarrow> gcd (k*m) n = gcd m n"
   oops