equal
deleted
inserted
replaced
1 (* Title: HOL/Algebra/Module.thy |
1 (* Title: HOL/Algebra/Module.thy |
2 Author: Clemens Ballarin, started 15 April 2003 |
2 Author: Clemens Ballarin, started 15 April 2003 |
3 Copyright: Clemens Ballarin |
3 Copyright: Clemens Ballarin |
4 *) |
4 *) |
5 |
5 |
6 theory Module imports Ring begin |
6 theory Module |
7 |
7 imports Ring |
|
8 begin |
8 |
9 |
9 section {* Modules over an Abelian Group *} |
10 section {* Modules over an Abelian Group *} |
10 |
11 |
11 subsection {* Definitions *} |
12 subsection {* Definitions *} |
12 |
13 |