equal
deleted
inserted
replaced
1 (* ID: $Id$ |
1 (* ID: $Id$ |
2 Author: Bernhard Haeupler |
2 Author: Bernhard Haeupler |
3 |
3 |
4 This theory is about the relative completeness of the tactic |
4 This theory is about of the relative completeness of method comm-ring |
5 As long as the reified atomic polynomials of type 'a pol |
5 method. As long as the reified atomic polynomials of type 'a pol are |
6 are in normal form, the cring method is complete *) |
6 in normal form, the cring method is complete. |
|
7 *) |
|
8 |
|
9 header {* Proof of the relative completeness of method comm-ring *} |
7 |
10 |
8 theory Commutative_Ring_Complete |
11 theory Commutative_Ring_Complete |
9 imports Main |
12 imports Main |
10 begin |
13 begin |
11 |
14 |