Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. avoid duplicate fact error on global_interpretation of residues
  2. avoid looping simplification for z2
Changeset 75963:884dbbc8e1b3 by haftmann:
avoid duplicate fact error on global_interpretation of residues
The file was modified NEWS (diff)
The file was modified src/HOL/Algebra/Ideal_Product.thy (diff)
The file was modified src/HOL/Algebra/Ring.thy (diff)
The file was modified src/HOL/Algebra/RingHom.thy (diff)
The file was modified src/HOL/Algebra/UnivPoly.thy (diff)
The file was modified src/HOL/Number_Theory/Residues.thy (diff)
Changeset 75962:c530cb79ccbc by haftmann:
avoid looping simplification for z2
The file was modified src/HOL/Library/Z2.thy (diff)
The file was modified src/HOL/Rings.thy (diff)