| changeset 60533 | 1e7ccd864b62 |
| parent 58889 | 5b7a9633cfa8 |
| child 64962 | bf41e1109db3 |
| 60532:7fb5b7dc8332 | 60533:1e7ccd864b62 |
|---|---|
1 (* Author: Bernhard Haeupler *) |
1 (* Author: Bernhard Haeupler *) |
2 |
2 |
3 section {* Some examples demonstrating the comm-ring method *} |
3 section \<open>Some examples demonstrating the comm-ring method\<close> |
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 |