# HG changeset patch
# User nipkow
# Date 1182783401 -7200
# Node ID 4db8aa43076cd4777942879e8f976f6a57ec1773
# Parent  94e7c8f823b55be0da46d94377eb9e1381afde5f
removed theorem

diff -r 94e7c8f823b5 -r 4db8aa43076c doc-src/TutorialI/Types/Numbers.thy
--- a/doc-src/TutorialI/Types/Numbers.thy	Mon Jun 25 15:19:34 2007 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy	Mon Jun 25 16:56:41 2007 +0200
@@ -244,9 +244,6 @@
 @{thm[display] mult_eq_0_iff[no_vars]}
 \rulename{mult_eq_0_iff}
 
-@{thm[display] field_mult_eq_0_iff[no_vars]}
-\rulename{field_mult_eq_0_iff}
-
 @{thm[display] mult_cancel_right[no_vars]}
 \rulename{mult_cancel_right}
 
diff -r 94e7c8f823b5 -r 4db8aa43076c doc-src/TutorialI/Types/document/Numbers.tex
--- a/doc-src/TutorialI/Types/document/Numbers.tex	Mon Jun 25 15:19:34 2007 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex	Mon Jun 25 16:56:41 2007 +0200
@@ -538,11 +538,6 @@
 \rulename{mult_eq_0_iff}
 
 \begin{isabelle}%
-{\isacharparenleft}a\ {\isacharasterisk}\ b\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ b\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharparenright}%
-\end{isabelle}
-\rulename{field_mult_eq_0_iff}
-
-\begin{isabelle}%
 {\isacharparenleft}a\ {\isacharasterisk}\ c\ {\isacharequal}\ b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
 \end{isabelle}
 \rulename{mult_cancel_right}