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