Summary
- added definitions multp{DM,HO} and corresponding lemmas
- added wfP_less to wellorder and wfP_less_multiset
The file was modified | src/HOL/Library/Multiset_Order.thy (diff) |
The file was modified | src/HOL/Library/Multiset.thy (diff) |
The file was modified | src/HOL/Wellfounded.thy (diff) |