equal
deleted
inserted
replaced
427 \rulename{mult_eq_0_iff}\isanewline |
427 \rulename{mult_eq_0_iff}\isanewline |
428 (a\ *\ c\ =\ b\ *\ c)\ =\ (c\ =\ (0::'a)\ \isasymor \ a\ =\ b) |
428 (a\ *\ c\ =\ b\ *\ c)\ =\ (c\ =\ (0::'a)\ \isasymor \ a\ =\ b) |
429 \rulename{mult_cancel_right} |
429 \rulename{mult_cancel_right} |
430 \end{isabelle} |
430 \end{isabelle} |
431 Theorems \isa{field_mult_eq_0_iff} and \isa{field_mult_cancel_right} |
431 Theorems \isa{field_mult_eq_0_iff} and \isa{field_mult_cancel_right} |
432 express the same properties, only for fields. When working with such |
432 express the same properties, only for fields. |
433 theorems, setting the \texttt{show_sorts}\index{*show_sorts (flag)} |
433 \begin{pgnote} |
434 flag will display the type classes of all type variables. Here is how the |
434 Setting the flag \textsf{Isabelle} $>$ \textsf{Settings} $>$ |
435 theorem \isa{field_mult_cancel_right} appears with the flag set. |
435 \textsf{Show Sorts} will display the type classes of all type variables. |
|
436 \end{pgnote} |
|
437 \noindent |
|
438 Here is how the theorem \isa{field_mult_cancel_right} appears with the flag set. |
436 \begin{isabelle} |
439 \begin{isabelle} |
437 ((a::'a::field)\ *\ (c::'a::field)\ =\ (b::'a::field)\ *\ c)\ =\isanewline |
440 ((a::'a::field)\ *\ (c::'a::field)\ =\ (b::'a::field)\ *\ c)\ =\isanewline |
438 (c\ =\ (0::'a::field)\ \isasymor \ a\ =\ b) |
441 (c\ =\ (0::'a::field)\ \isasymor \ a\ =\ b) |
439 \end{isabelle} |
442 \end{isabelle} |
440 |
443 |