Summary
- Tuned multiset lattice
- More lemmas on Gcd/Lcm
- Conditionally complete lattice of multisets
The file was modified | src/HOL/Library/Multiset.thy (diff) |
The file was modified | src/HOL/GCD.thy (diff) |
The file was modified | src/HOL/Rings.thy (diff) |
The file was modified | src/HOL/Library/Multiset.thy (diff) |