equal
deleted
inserted
replaced
3 Copyright: Clemens Ballarin |
3 Copyright: Clemens Ballarin |
4 *) |
4 *) |
5 |
5 |
6 theory Ring |
6 theory Ring |
7 imports FiniteProduct |
7 imports FiniteProduct |
8 uses ("ringsimp.ML") |
|
9 begin |
8 begin |
10 |
9 |
11 section {* The Algebraic Hierarchy of Rings *} |
10 section {* The Algebraic Hierarchy of Rings *} |
12 |
11 |
13 subsection {* Abelian Groups *} |
12 subsection {* Abelian Groups *} |
387 by (simp only: a_minus_def) |
386 by (simp only: a_minus_def) |
388 |
387 |
389 text {* Setup algebra method: |
388 text {* Setup algebra method: |
390 compute distributive normal form in locale contexts *} |
389 compute distributive normal form in locale contexts *} |
391 |
390 |
392 use "ringsimp.ML" |
391 ML_file "ringsimp.ML" |
393 |
392 |
394 setup Algebra.attrib_setup |
393 setup Algebra.attrib_setup |
395 |
394 |
396 method_setup algebra = {* |
395 method_setup algebra = {* |
397 Scan.succeed (SIMPLE_METHOD' o Algebra.algebra_tac) |
396 Scan.succeed (SIMPLE_METHOD' o Algebra.algebra_tac) |