equal
deleted
inserted
replaced
220 thm "minus_minus", thm "minus0", thm "a_lcomm", thm "m_lcomm", (*thm "r_one",*) |
220 thm "minus_minus", thm "minus0", thm "a_lcomm", thm "m_lcomm", (*thm "r_one",*) |
221 thm "r_distr", thm "l_null", thm "r_null", thm "l_minus", thm "r_minus"]; |
221 thm "r_distr", thm "l_null", thm "r_null", thm "l_minus", thm "r_minus"]; |
222 *} (* Note: r_one is not necessary in ring_ss *) |
222 *} (* Note: r_one is not necessary in ring_ss *) |
223 |
223 |
224 method_setup ring = |
224 method_setup ring = |
225 {* Method.no_args (Method.SIMPLE_METHOD' (full_simp_tac ring_ss)) *} |
225 {* Method.no_args (SIMPLE_METHOD' (full_simp_tac ring_ss)) *} |
226 {* computes distributive normal form in rings *} |
226 {* computes distributive normal form in rings *} |
227 |
227 |
228 |
228 |
229 subsection {* Rings and the summation operator *} |
229 subsection {* Rings and the summation operator *} |
230 |
230 |