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