| author | wenzelm | 
| Sat, 08 Sep 2018 22:43:25 +0200 | |
| changeset 68955 | 0851db8cde12 | 
| 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 |