equal
deleted
inserted
replaced
3 Author: Gertrud Bauer and Markus Wenzel, TU Muenchen |
3 Author: Gertrud Bauer and Markus Wenzel, TU Muenchen |
4 Lawrence C Paulson, University of Cambridge |
4 Lawrence C Paulson, University of Cambridge |
5 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 License: GPL (GNU GENERAL PUBLIC LICENSE) |
6 *) |
6 *) |
7 |
7 |
8 header {* |
8 header {* Ring and field structures *} |
9 \title{Ring and field structures} |
|
10 \author{Gertrud Bauer, L. C. Paulson and Markus Wenzel} |
|
11 *} |
|
12 |
9 |
13 theory Ring_and_Field = Inductive: |
10 theory Ring_and_Field = Inductive: |
14 |
11 |
15 subsection {* Abstract algebraic structures *} |
12 subsection {* Abstract algebraic structures *} |
16 |
13 |