# HG changeset patch
# User huffman
# Date 1332930504 -7200
# Node ID f760e15343bc70e0e61d0b3ef56898e2b44facd2
# Parent  d81ee6c5209a8118d3de3c4e568990fac1957cfd
removed references to obsolete theorems

diff -r d81ee6c5209a -r f760e15343bc doc-src/TutorialI/Types/Numbers.thy
--- a/doc-src/TutorialI/Types/Numbers.thy	Wed Mar 28 11:40:12 2012 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy	Wed Mar 28 12:28:24 2012 +0200
@@ -25,9 +25,6 @@
 *}
 
 text{*
-@{thm[display] numeral_0_eq_0[no_vars]}
-\rulename{numeral_0_eq_0}
-
 @{thm[display] numeral_1_eq_1[no_vars]}
 \rulename{numeral_1_eq_1}
 
@@ -67,8 +64,8 @@
 @{thm[display] diff_mult_distrib[no_vars]}
 \rulename{diff_mult_distrib}
 
-@{thm[display] mod_mult_distrib[no_vars]}
-\rulename{mod_mult_distrib}
+@{thm[display] mult_mod_left[no_vars]}
+\rulename{mult_mod_left}
 
 @{thm[display] nat_diff_split[no_vars]}
 \rulename{nat_diff_split}
@@ -152,8 +149,8 @@
 @{thm[display] zdiv_zmult1_eq[no_vars]}
 \rulename{zdiv_zmult1_eq}
 
-@{thm[display] zmod_zmult1_eq[no_vars]}
-\rulename{zmod_zmult1_eq}
+@{thm[display] mod_mult_right_eq[no_vars]}
+\rulename{mod_mult_right_eq}
 
 @{thm[display] zdiv_zmult2_eq[no_vars]}
 \rulename{zdiv_zmult2_eq}
diff -r d81ee6c5209a -r f760e15343bc doc-src/TutorialI/Types/document/Numbers.tex
--- a/doc-src/TutorialI/Types/document/Numbers.tex	Wed Mar 28 11:40:12 2012 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex	Wed Mar 28 12:28:24 2012 +0200
@@ -75,11 +75,6 @@
 %
 \begin{isamarkuptext}%
 \begin{isabelle}%
-Numeral{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}%
-\end{isabelle}
-\rulename{numeral_0_eq_0}
-
-\begin{isabelle}%
 Numeral{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}%
 \end{isabelle}
 \rulename{numeral_1_eq_1}
@@ -156,9 +151,9 @@
 \rulename{diff_mult_distrib}
 
 \begin{isabelle}%
-m\ mod\ n\ {\isaliteral{2A}{\isacharasterisk}}\ k\ {\isaliteral{3D}{\isacharequal}}\ m\ {\isaliteral{2A}{\isacharasterisk}}\ k\ mod\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2A}{\isacharasterisk}}\ k{\isaliteral{29}{\isacharparenright}}%
+a\ mod\ b\ {\isaliteral{2A}{\isacharasterisk}}\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ c\ mod\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}%
 \end{isabelle}
-\rulename{mod_mult_distrib}
+\rulename{mult_mod_left}
 
 \begin{isabelle}%
 P\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2D}{\isacharminus}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{3C}{\isacharless}}\ b\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}d{\isaliteral{2E}{\isachardot}}\ a\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2B}{\isacharplus}}\ d\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ d{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
@@ -326,7 +321,7 @@
 \begin{isabelle}%
 a\ {\isaliteral{2A}{\isacharasterisk}}\ b\ mod\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ mod\ c%
 \end{isabelle}
-\rulename{zmod_zmult1_eq}
+\rulename{mod_mult_right_eq}
 
 \begin{isabelle}%
 {\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ div\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ div\ b\ div\ c%