Skip to content
Failed

Changes

Summary

  1. theory Poly_Mapping
  2. new theory Library/Poly_Mapping, of almost-everywhere-zero functions
  3. Material concerning exact sequences of groups
  4. Products and sums of a family of groups
  5. new group theory material, mostly ported from HOL Light
Changeset 70043:350acd367028 by paulson _lp15@cam.ac.uk_:
theory Poly_Mapping
The file was addedsrc/HOL/Library/Poly_Mapping.thy
Changeset 70042:45787384ff86 by paulson _lp15@cam.ac.uk_:
new theory Library/Poly_Mapping, of almost-everywhere-zero functions
The file was modified src/HOL/Library/Library.thy (diff)
Changeset 70041:2b23dd163c7f by paulson _lp15@cam.ac.uk_:
Material concerning exact sequences of groups
The file was modified src/HOL/Algebra/Exact_Sequence.thy (diff)
Changeset 70040:6a9e2a82ea15 by paulson _lp15@cam.ac.uk_:
Products and sums of a family of groups
The file was addedsrc/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)
Changeset 70039:733e256ecdf3 by paulson _lp15@cam.ac.uk_:
new group theory material, mostly ported from HOL Light
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)