| author | haftmann |
| Thu, 31 Jan 2019 13:08:59 +0000 | |
| changeset 69768 | 7e4966eaf781 |
| parent 68582 | b9b9e2985878 |
| child 70027 | 94494b92d8d0 |
| permissions | -rw-r--r-- |
| 68582 | 1 |
(* Title: HOL/Algebra/Algebra.thy *) |
|
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
2 |
|
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
3 |
theory Algebra |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
4 |
imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields |
| 68578 | 5 |
Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials |
|
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
6 |
begin |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
7 |
end |