# HG changeset patch
# User haftmann
# Date 1216545548 -7200
# Node ID 674496eb5965033a80e46e9557ceb095ed314f84
# Parent  0efc8b68ee4ab18d272ba29329835d650310bd03
(adjusted)

diff -r 0efc8b68ee4a -r 674496eb5965 doc-src/TutorialI/Rules/Forward.thy
--- a/doc-src/TutorialI/Rules/Forward.thy	Sun Jul 20 11:10:04 2008 +0200
+++ b/doc-src/TutorialI/Rules/Forward.thy	Sun Jul 20 11:19:08 2008 +0200
@@ -192,8 +192,7 @@
 *)
 
 lemma relprime_dvd_mult_iff: "gcd k n = 1 \<Longrightarrow> (k dvd m*n) = (k dvd m)";
-by (blast intro: relprime_dvd_mult dvd_trans)
-
+by (auto intro: relprime_dvd_mult elim: dvdE)
 
 lemma relprime_20_81: "gcd 20 81 = 1";
 by (simp add: gcd.simps)
diff -r 0efc8b68ee4a -r 674496eb5965 doc-src/TutorialI/Types/Numbers.thy
--- a/doc-src/TutorialI/Types/Numbers.thy	Sun Jul 20 11:10:04 2008 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy	Sun Jul 20 11:19:08 2008 +0200
@@ -113,11 +113,11 @@
 @{thm[display] div_mult_mult1[no_vars]}
 \rulename{div_mult_mult1}
 
-@{thm[display] DIVISION_BY_ZERO_DIV[no_vars]}
-\rulename{DIVISION_BY_ZERO_DIV}
+@{thm[display] div_by_0 [no_vars]}
+\rulename{div_by_0}
 
-@{thm[display] DIVISION_BY_ZERO_MOD[no_vars]}
-\rulename{DIVISION_BY_ZERO_MOD}
+@{thm[display] mod_by_0 [no_vars]}
+\rulename{mod_by_0}
 
 @{thm[display] dvd_anti_sym[no_vars]}
 \rulename{dvd_anti_sym}
diff -r 0efc8b68ee4a -r 674496eb5965 doc-src/TutorialI/Types/document/Numbers.tex
--- a/doc-src/TutorialI/Types/document/Numbers.tex	Sun Jul 20 11:10:04 2008 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex	Sun Jul 20 11:19:08 2008 +0200
@@ -232,7 +232,7 @@
 \rulename{mod_if}
 
 \begin{isabelle}%
-m\ div\ n\ {\isacharasterisk}\ n\ {\isacharplus}\ m\ mod\ n\ {\isacharequal}\ m%
+a\ div\ b\ {\isacharasterisk}\ b\ {\isacharplus}\ a\ mod\ b\ {\isacharequal}\ a%
 \end{isabelle}
 \rulename{mod_div_equality}
 
@@ -263,14 +263,14 @@
 \rulename{div_mult_mult1}
 
 \begin{isabelle}%
-a\ div\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}%
+a\ div\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}%
 \end{isabelle}
-\rulename{DIVISION_BY_ZERO_DIV}
+\rulename{div_by_0}
 
 \begin{isabelle}%
-a\ mod\ {\isadigit{0}}\ {\isacharequal}\ a%
+a\ mod\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ a%
 \end{isabelle}
-\rulename{DIVISION_BY_ZERO_MOD}
+\rulename{mod_by_0}
 
 \begin{isabelle}%
 {\isasymlbrakk}m\ dvd\ n{\isacharsemicolon}\ n\ dvd\ m{\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n%
@@ -278,7 +278,7 @@
 \rulename{dvd_anti_sym}
 
 \begin{isabelle}%
-{\isasymlbrakk}k\ dvd\ m{\isacharsemicolon}\ k\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ k\ dvd\ m\ {\isacharplus}\ n%
+{\isasymlbrakk}a\ dvd\ b{\isacharsemicolon}\ a\ dvd\ c{\isasymrbrakk}\ {\isasymLongrightarrow}\ a\ dvd\ b\ {\isacharplus}\ c%
 \end{isabelle}
 \rulename{dvd_add}