Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. generalized some lemmas on multisets
  2. rule out pathologic instances
  3. tuned some proofs and added some lemmas
Changeset 66938:c78ff0aeba4c by haftmann:
generalized some lemmas on multisets
The file was modified src/HOL/Computational_Algebra/Factorial_Ring.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
Changeset 66937:a1a4a5e2933a by haftmann:
rule out pathologic instances
The file was modified NEWS (diff)
The file was modified src/HOL/Rings.thy (diff)
Changeset 66936:cf8d8fc23891 by haftmann:
tuned some proofs and added some lemmas
The file was modified src/HOL/Analysis/Gamma_Function.thy (diff)
The file was modified src/HOL/GCD.thy (diff)
The file was modified src/HOL/Groups_Big.thy (diff)
The file was modified src/HOL/Inequalities.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
The file was modified src/HOL/Library/Extended_Real.thy (diff)
The file was modified src/HOL/Library/Numeral_Type.thy (diff)
The file was modified src/HOL/Library/Uprod.thy (diff)
The file was modified src/HOL/Nat.thy (diff)
The file was modified src/HOL/Num.thy (diff)
The file was modified src/HOL/Orderings.thy (diff)
The file was modified src/HOL/Power.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
The file was modified src/HOL/ex/Function_Growth.thy (diff)