| changeset 68552 | 391e89e03eef |
| parent 68551 | b680e74eb6f2 |
| child 68582 | b9b9e2985878 |
| 68551:b680e74eb6f2 | 68552:391e89e03eef |
|---|---|
1 (* Title: HOL/Algebra/Ring.thy |
1 (* Title: HOL/Algebra/Ring.thy |
2 Author: Clemens Ballarin, started 9 December 1996 |
2 Author: Clemens Ballarin, started 9 December 1996 |
3 Copyright: Clemens Ballarin |
3 |
4 With contributions by Martin Baillon |
|
4 *) |
5 *) |
5 |
6 |
6 theory Ring |
7 theory Ring |
7 imports FiniteProduct |
8 imports FiniteProduct |
8 begin |
9 begin |