Summary
- generalized some lemmas on multisets
- rule out pathologic instances
- tuned some proofs and added some lemmas
The file was modified | src/HOL/Computational_Algebra/Factorial_Ring.thy (diff) |
The file was modified | src/HOL/Library/Multiset.thy (diff) |
The file was modified | NEWS (diff) |
The file was modified | src/HOL/Rings.thy (diff) |
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) |