isabelle: src/HOL/Algebra/Algebra.thy@6cc3b131f761 (annotated)

68582 b9b9e2985878 more standard headers; wenzelm parents: 68578 diff changeset	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
70063 adaa0a6ea4fe fixes for Free_Abelian_Groups paulson <lp15@cam.ac.uk> parents: 70040 diff changeset	4	imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Free_Abelian_Groups
70160 8e9100dcde52 Towards a proof of algebraic closure (NB not finished) paulson <lp15@cam.ac.uk> parents: 70063 diff changeset	5	Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials Algebraic_Closure
77089 b4f892d0625d Some new material from the AFP paulson <lp15@cam.ac.uk> parents: 70160 diff changeset	6	Left_Coset
68569 c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena paulson <lp15@cam.ac.uk> parents: diff changeset	7	begin
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena paulson <lp15@cam.ac.uk> parents: diff changeset	8	end