--- 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