Summary
- theory Poly_Mapping
- new theory Library/Poly_Mapping, of almost-everywhere-zero functions
- Material concerning exact sequences of groups
- Products and sums of a family of groups
- new group theory material, mostly ported from HOL Light
The file was added | src/HOL/Library/Poly_Mapping.thy |
The file was modified | src/HOL/Library/Library.thy (diff) |
The file was modified | src/HOL/Algebra/Exact_Sequence.thy (diff) |
The file was added | src/HOL/Algebra/Product_Groups.thy |
The file was modified | src/HOL/Algebra/Algebra.thy (diff) |
The file was modified | src/HOL/Algebra/Group.thy (diff) |
The file was modified | src/HOL/Algebra/Coset.thy (diff) |
The file was modified | src/HOL/Algebra/Elementary_Groups.thy (diff) |
The file was modified | src/HOL/Algebra/Generated_Groups.thy (diff) |
The file was modified | src/HOL/Algebra/Group.thy (diff) |