| changeset 58889 | 5b7a9633cfa8 |
| parent 49070 | f00fee6d21d4 |
| child 60533 | 1e7ccd864b62 |
| 58888:9537bf1c4853 | 58889:5b7a9633cfa8 |
|---|---|
1 (* Author: Bernhard Haeupler *) |
1 (* Author: Bernhard Haeupler *) |
2 |
2 |
3 header {* Some examples demonstrating the comm-ring method *} |
3 section {* Some examples demonstrating the comm-ring method *} |
4 |
4 |
5 theory Commutative_Ring_Ex |
5 theory Commutative_Ring_Ex |
6 imports "../Commutative_Ring" |
6 imports "../Commutative_Ring" |
7 begin |
7 begin |
8 |
8 |