equal
deleted
inserted
replaced
1 (* Author: Bernhard Haeupler *) |
1 (* Author: Bernhard Haeupler *) |
2 |
2 |
3 header {* Some examples demonstrating the comm-ring method *} |
3 header {* 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 |
9 lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243" |
9 lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243" |
10 by comm_ring |
10 by comm_ring |
11 |
11 |