1.1 --- a/doc-src/TutorialI/Rules/Primes.thy	Wed Nov 18 14:00:08 2009 +0100
     1.2 +++ b/doc-src/TutorialI/Rules/Primes.thy	Thu Nov 19 08:19:57 2009 +0100
     1.3 @@ -112,13 +112,13 @@
     1.4  (*uniqueness of GCDs*)
     1.5  lemma is_gcd_unique: "\<lbrakk> is_gcd m a b; is_gcd n a b \<rbrakk> \<Longrightarrow> m=n"
     1.6  apply (simp add: is_gcd_def);
     1.7 -apply (blast intro: dvd_anti_sym)
     1.8 +apply (blast intro: dvd_antisym)
     1.9  done
    1.10  
    1.11  
    1.12  text {*
    1.13 -@{thm[display] dvd_anti_sym}
    1.14 -\rulename{dvd_anti_sym}
    1.15 +@{thm[display] dvd_antisym}
    1.16 +\rulename{dvd_antisym}
    1.17  
    1.18  \begin{isabelle}
    1.19  proof\ (prove):\ step\ 1\isanewline
    1.20 @@ -154,7 +154,7 @@
    1.21    apply (auto intro: dvd_trans [of _ m])
    1.22    done
    1.23  
    1.24 -(*This is half of the proof (by dvd_anti_sym) of*)
    1.25 +(*This is half of the proof (by dvd_antisym) of*)
    1.26  lemma gcd_mult_cancel: "gcd k n = 1 \<Longrightarrow> gcd (k*m) n = gcd m n"
    1.27    oops
    1.28