Skip to content
Failed

Changes

Summary

  1. 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
Changeset 62430:9527ff088c15 by haftmann:
more succint formulation of membership for multisets, similar to lists;<br>discontinued ASCII notation for multiset membership;<br>more theorems on multisets, dropping redundant interpretation;<br>modernized notation;<br>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)