--- 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
--- a/doc-src/TutorialI/Types/Numbers.thy Wed Nov 18 14:00:08 2009 +0100
+++ b/doc-src/TutorialI/Types/Numbers.thy Thu Nov 19 08:19:57 2009 +0100
@@ -118,8 +118,8 @@
@{thm[display] mod_by_0 [no_vars]}
\rulename{mod_by_0}
-@{thm[display] dvd_anti_sym[no_vars]}
-\rulename{dvd_anti_sym}
+@{thm[display] dvd_antisym[no_vars]}
+\rulename{dvd_antisym}
@{thm[display] dvd_add[no_vars]}
\rulename{dvd_add}
--- a/doc-src/TutorialI/Types/document/Numbers.tex Wed Nov 18 14:00:08 2009 +0100
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Thu Nov 19 08:19:57 2009 +0100
@@ -274,7 +274,7 @@
\begin{isabelle}%
{\isasymlbrakk}m\ dvd\ n{\isacharsemicolon}\ n\ dvd\ m{\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n%
\end{isabelle}
-\rulename{dvd_anti_sym}
+\rulename{dvd_antisym}
\begin{isabelle}%
{\isasymlbrakk}a\ dvd\ b{\isacharsemicolon}\ a\ dvd\ c{\isasymrbrakk}\ {\isasymLongrightarrow}\ a\ dvd\ b\ {\isacharplus}\ c%
--- a/doc-src/TutorialI/Types/numerics.tex Wed Nov 18 14:00:08 2009 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex Thu Nov 19 08:19:57 2009 +0100
@@ -1,4 +1,3 @@
-
\section{Numbers}
\label{sec:numbers}
@@ -192,7 +191,7 @@
relation. Here are some of the facts proved about it:
\begin{isabelle}
\isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%
-\rulenamedx{dvd_anti_sym}\isanewline
+\rulenamedx{dvd_antisym}\isanewline
\isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)
\rulenamedx{dvd_add}
\end{isabelle}