Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. auto update;
  2. merged
  3. Adjusting Number_Theory for new Algebra
  4. merged
  5. reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
  6. merged
  7. New material from Martin Baillon and Paulo Emílio de Vilhena
  8. tuned
  9. removed duplicates
Changeset 68449:6d0f1a5a16ea by wenzelm:
auto update;
The file was modified src/Tools/VSCode/extension/package.json (diff)
Changeset 68448:3d1517f3ba49 by paulson:
merged
Changeset 68447:0beb927eed89 by paulson _lp15@cam.ac.uk_:
Adjusting Number_Theory for new Algebra
The file was modified src/HOL/Algebra/FiniteProduct.thy (diff)
The file was modified src/HOL/Number_Theory/Residues.thy (diff)
Changeset 68446:92ddca1edc43 by paulson:
merged
Changeset 68445:c183a6a69f2d by paulson _lp15@cam.ac.uk_:
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
The file was modified src/HOL/Algebra/Coset.thy (diff)
The file was modified src/HOL/Algebra/FiniteProduct.thy (diff)
The file was modified src/HOL/Algebra/Group.thy (diff)
The file was modified src/HOL/Algebra/Group_Action.thy (diff)
The file was modified src/HOL/Algebra/Ideal.thy (diff)
The file was modified src/HOL/Algebra/Multiplicative_Group.thy (diff)
The file was modified src/HOL/Algebra/Ring.thy (diff)
The file was modified src/HOL/Algebra/Sylow.thy (diff)
The file was modified src/HOL/Algebra/UnivPoly.thy (diff)
The file was modified src/HOL/Algebra/Zassenhaus.thy (diff)
The file was modified src/HOL/ROOT (diff)
The file was removedsrc/HOL/Algebra/More_Finite_Product.thy
The file was removedsrc/HOL/Algebra/More_Group.thy
The file was removedsrc/HOL/Algebra/More_Ring.thy
Changeset 68444:ff61cbfb3f2d by paulson:
merged
Changeset 68443:43055b016688 by paulson _lp15@cam.ac.uk_:
New material from Martin Baillon and Paulo Emílio de Vilhena
The file was addedsrc/HOL/Algebra/Group_Action.thy
The file was addedsrc/HOL/Algebra/Zassenhaus.thy
The file was modified src/HOL/Algebra/AbelCoset.thy (diff)
The file was modified src/HOL/Algebra/Congruence.thy (diff)
The file was modified src/HOL/Algebra/Coset.thy (diff)
The file was modified src/HOL/Algebra/Group.thy (diff)
The file was modified src/HOL/Algebra/Ideal.thy (diff)
The file was modified src/HOL/Algebra/Ring.thy (diff)
The file was modified src/HOL/Algebra/Sylow.thy (diff)
The file was modified src/HOL/ROOT (diff)
Changeset 68442:477b3f7067c9 by nipkow:
tuned
The file was modified src/HOL/Computational_Algebra/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy (diff)
The file was modified src/HOL/Decision_Procs/Rat_Pair.thy (diff)
The file was modified src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy (diff)
Changeset 68441:3b11d48a711a by nipkow:
removed duplicates
The file was modified src/HOL/Rat.thy (diff)