equal
deleted
inserted
replaced
1 (* $Id$ *) |
1 (* ID: $Id$ |
|
2 Author: Bernhard Haeupler |
|
3 *) |
|
4 |
|
5 header {* Some examples demonstrating the comm-ring method *} |
|
6 |
2 theory Commutative_RingEx |
7 theory Commutative_RingEx |
3 imports Main |
8 imports Main |
4 begin |
9 begin |
5 |
|
6 (* Some examples demonstrating the comm_ring method *) |
|
7 |
10 |
8 lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243" |
11 lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243" |
9 by comm_ring |
12 by comm_ring |
10 |
13 |
11 lemma "((x::int) + y)^2 = x^2 + y^2 + 2*x*y" |
14 lemma "((x::int) + y)^2 = x^2 + y^2 + 2*x*y" |