author nipkow Thu, 19 Nov 2009 08:19:57 +0100 changeset 33750 0a0d6d79d984 parent 33749 8aab63a91053 child 33751 7ead0ccf6cbd child 33752 9aa8e961f850 child 33804 39b494e8c055
anti_sym -> antisym
--- 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 (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}

\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)
\end{isabelle}