equal
deleted
inserted
replaced
389 text {* Setup algebra method: |
389 text {* Setup algebra method: |
390 compute distributive normal form in locale contexts *} |
390 compute distributive normal form in locale contexts *} |
391 |
391 |
392 use "ringsimp.ML" |
392 use "ringsimp.ML" |
393 |
393 |
394 setup Algebra.setup |
394 setup Algebra.attrib_setup |
|
395 |
|
396 method_setup algebra = {* |
|
397 Scan.succeed (SIMPLE_METHOD' o Algebra.algebra_tac) |
|
398 *} "normalisation of algebraic structure" |
395 |
399 |
396 lemmas (in ring) ring_simprules |
400 lemmas (in ring) ring_simprules |
397 [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] = |
401 [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] = |
398 a_closed zero_closed a_inv_closed minus_closed m_closed one_closed |
402 a_closed zero_closed a_inv_closed minus_closed m_closed one_closed |
399 a_assoc l_zero l_neg a_comm m_assoc l_one l_distr minus_eq |
403 a_assoc l_zero l_neg a_comm m_assoc l_one l_distr minus_eq |