Summary
- more succint formulation of membership for multisets, similar to lists; discontinued ASCII notation for multiset membership; more theorems on multisets, dropping redundant interpretation; modernized notation; some annotations concerning future work
The file was modified | NEWS (diff) |
The file was modified | src/HOL/Algebra/Divisibility.thy (diff) |
The file was modified | src/HOL/Library/Multiset.thy (diff) |
The file was modified | src/HOL/Library/Multiset_Order.thy (diff) |
The file was modified | src/HOL/Number_Theory/UniqueFactorization.thy (diff) |
The file was modified | src/HOL/UNITY/Comp/AllocBase.thy (diff) |
The file was modified | src/HOL/UNITY/Follows.thy (diff) |
The file was modified | src/HOL/ex/Quicksort.thy (diff) |