# 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 \ (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}