# HG changeset patch
# User nipkow
# Date 1258615197 -3600
# Node ID 0a0d6d79d984fe99052b8642d51e51b07abaf7a5
# Parent  8aab63a9105343333bc6423645c7f16e61953be7
anti_sym -> antisym

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
 
diff -r 8aab63a91053 -r 0a0d6d79d984 doc-src/TutorialI/Types/Numbers.thy
--- 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}
diff -r 8aab63a91053 -r 0a0d6d79d984 doc-src/TutorialI/Types/document/Numbers.tex
--- 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%
diff -r 8aab63a91053 -r 0a0d6d79d984 doc-src/TutorialI/Types/numerics.tex
--- 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}