changeset 37743 | 3daaf23b9ab4 |
parent 35267 | 8dfd816713c6 |
child 39093 | 4abe644fcea5 |
37742:0a3fa8fbcdc5 | 37743:3daaf23b9ab4 |
---|---|
1 (* Author: Amine Chaieb |
1 (* Title: HOL/Decision_Procs/commutative_ring_tac.ML |
2 Author: Amine Chaieb |
|
2 |
3 |
3 Tactic for solving equalities over commutative rings. |
4 Tactic for solving equalities over commutative rings. |
4 *) |
5 *) |
5 |
6 |
6 signature COMMUTATIVE_RING_TAC = |
7 signature COMMUTATIVE_RING_TAC = |