equal
deleted
inserted
replaced
|
1 (* Title: HOL/Algebra/Algebra *) |
|
2 |
|
3 theory Algebra |
|
4 imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields |
|
5 Divisibility Embedded_Algebras IntRing Sym_Groups |
|
6 (*Frobenius Exact_Sequence Polynomials*) |
|
7 begin |
|
8 end |