1.1 --- a/doc-src/TutorialI/Types/Numbers.thy	Tue Jun 26 13:02:28 2007 +0200
     1.2 +++ b/doc-src/TutorialI/Types/Numbers.thy	Tue Jun 26 15:48:09 2007 +0200
     1.3 @@ -246,12 +246,18 @@
     1.4  
     1.5  @{thm[display] mult_cancel_right[no_vars]}
     1.6  \rulename{mult_cancel_right}
     1.7 +
     1.8 +@{thm[display] mult_cancel_left[no_vars]}
     1.9 +\rulename{mult_cancel_left}
    1.10  *}
    1.11  
    1.12  ML{*set show_sorts*}
    1.13  
    1.14  text{*
    1.15  effect of show sorts on the above
    1.16 +
    1.17 +@{thm[display] mult_cancel_left[no_vars]}
    1.18 +\rulename{mult_cancel_left}
    1.19  *}
    1.20  
    1.21  ML{*reset show_sorts*}

     2.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex	Tue Jun 26 13:02:28 2007 +0200
     2.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex	Tue Jun 26 15:48:09 2007 +0200
     2.3 @@ -543,9 +543,9 @@
     2.4  \rulename{mult_cancel_right}
     2.5  
     2.6  \begin{isabelle}%
     2.7 -{\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.8 +{\isacharparenleft}c\ {\isacharasterisk}\ a\ {\isacharequal}\ c\ {\isacharasterisk}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
     2.9  \end{isabelle}
    2.10 -\rulename{field_mult_cancel_right}%
    2.11 +\rulename{mult_cancel_left}%
    2.12  \end{isamarkuptext}%
    2.13  \isamarkuptrue%
    2.14  %
    2.15 @@ -567,11 +567,11 @@
    2.16  effect of show sorts on the above
    2.17  
    2.18  \begin{isabelle}%
    2.19 -{\isacharparenleft}{\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isasymColon}division{\isacharunderscore}ring{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}c{\isasymColon}{\isacharprime}a{\isasymColon}division{\isacharunderscore}ring{\isacharparenright}\ {\isacharequal}\isanewline
    2.20 -\isaindent{{\isacharparenleft}}{\isacharparenleft}b{\isasymColon}{\isacharprime}a{\isasymColon}division{\isacharunderscore}ring{\isacharparenright}\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\isanewline
    2.21 -{\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isasymColon}division{\isacharunderscore}ring{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
    2.22 +{\isacharparenleft}{\isacharparenleft}c{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isacharequal}\isanewline
    2.23 +\isaindent{{\isacharparenleft}}c\ {\isacharasterisk}\ {\isacharparenleft}b{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
    2.24 +{\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
    2.25  \end{isabelle}
    2.26 -\rulename{field_mult_cancel_right}%
    2.27 +\rulename{mult_cancel_left}%
    2.28  \end{isamarkuptext}%
    2.29  \isamarkuptrue%
    2.30  %

     3.1 --- a/doc-src/TutorialI/Types/numerics.tex	Tue Jun 26 13:02:28 2007 +0200
     3.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Tue Jun 26 15:48:09 2007 +0200
     3.3 @@ -419,26 +419,23 @@
     3.4  Obviously, all properties involving orderings required an ordered
     3.5  structure.
     3.6  
     3.7 -The following two theorems are less obvious. Although they
     3.8 -mention no ordering, they require an ordered ring. However, if we have a 
     3.9 -field, then an ordering is no longer required.
    3.10 +The class \tcdx{ring_no_zero_divisors} of rings without zero divisors satisfies a number of natural cancellation laws, the first of which characterizes this class:
    3.11  \begin{isabelle}
    3.12  (a\ *\ b\ =\ (0::'a))\ =\ (a\ =\ (0::'a)\ \isasymor \ b\ =\ (0::'a))
    3.13  \rulename{mult_eq_0_iff}\isanewline
    3.14  (a\ *\ c\ =\ b\ *\ c)\ =\ (c\ =\ (0::'a)\ \isasymor \ a\ =\ b)
    3.15  \rulename{mult_cancel_right}
    3.16  \end{isabelle}
    3.17 -Theorems \isa{field_mult_eq_0_iff} and \isa{field_mult_cancel_right}
    3.18 -express the same properties, only for fields.
    3.19  \begin{pgnote}
    3.20  Setting the flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$
    3.21  \pgmenu{Show Sorts} will display the type classes of all type variables.
    3.22  \end{pgnote}
    3.23  \noindent
    3.24 -Here is how the theorem \isa{field_mult_cancel_right} appears with the flag set.
    3.25 +Here is how the theorem \isa{mult_cancel_left} appears with the flag set.
    3.26  \begin{isabelle}
    3.27 -((a::'a::field)\ *\ (c::'a::field)\ =\ (b::'a::field)\ *\ c)\ =\isanewline
    3.28 -(c\ =\ (0::'a::field)\ \isasymor \ a\ =\ b)
    3.29 +((c::'a::ring_no_zero_divisors)\ *\ (a::'a::ring_no_zero_divisors) =\isanewline
    3.30 +\ c\ *\ (b::'a::ring_no_zero_divisors))\ =\isanewline
    3.31 +(c\ =\ (0::'a::ring_no_zero_divisors)\ \isasymor\ a\ =\ b)
    3.32  \end{isabelle}
    3.33  
    3.34