1.1 --- a/doc-src/TutorialI/Types/Numbers.thy	Mon Jun 25 15:19:34 2007 +0200
     1.2 +++ b/doc-src/TutorialI/Types/Numbers.thy	Mon Jun 25 16:56:41 2007 +0200
     1.3 @@ -244,9 +244,6 @@
     1.4  @{thm[display] mult_eq_0_iff[no_vars]}
     1.5  \rulename{mult_eq_0_iff}
     1.6  
     1.7 -@{thm[display] field_mult_eq_0_iff[no_vars]}
     1.8 -\rulename{field_mult_eq_0_iff}
     1.9 -
    1.10  @{thm[display] mult_cancel_right[no_vars]}
    1.11  \rulename{mult_cancel_right}
    1.12  

     2.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex	Mon Jun 25 15:19:34 2007 +0200
     2.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex	Mon Jun 25 16:56:41 2007 +0200
     2.3 @@ -538,11 +538,6 @@
     2.4  \rulename{mult_eq_0_iff}
     2.5  
     2.6  \begin{isabelle}%
     2.7 -{\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}%
     2.8 -\end{isabelle}
     2.9 -\rulename{field_mult_eq_0_iff}
    2.10 -
    2.11 -\begin{isabelle}%
    2.12  {\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}%
    2.13  \end{isabelle}
    2.14  \rulename{mult_cancel_right}