--- 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)
--- 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}
--- 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}