Changes

Summary

Changeset 73594:5c4a09c4bc9c by haftmann: collecting more lemmas concerning multisets
The file was modified	`src/HOL/Fun.thy`
The file was modified	`src/HOL/Library/Multiset.thy`

Changeset 11741:28fe4ca859cd by haftmann: collecting more lemmas concerning multisets
The file was added	`thys/Berlekamp_Zassenhaus/More_Missing_Multiset.thy`
The file was added	`thys/Nested_Multisets_Ordinals/Duplicate_Free_Multiset.thy`
The file was added	`thys/PAC_Checker/PAC_Misc.thy`
The file was modified	`thys/Algebraic_Numbers/Algebraic_Numbers.thy`
The file was modified	`thys/Berlekamp_Zassenhaus/Poly_Mod_Finite_Field.thy`
The file was modified	`thys/Berlekamp_Zassenhaus/Unique_Factorization.thy`
The file was modified	`thys/Nested_Multisets_Ordinals/Multiset_More.thy`
The file was modified	`thys/Ordered_Resolution_Prover/Standard_Redundancy.thy`
The file was modified	`thys/PAC_Checker/Finite_Map_Multiset.thy`
The file was modified	`thys/PAC_Checker/PAC_Checker.thy`
The file was modified	`thys/PAC_Checker/ROOT`
The file was modified	`thys/PAC_Checker/WB_Sort.thy`
The file was modified	`thys/Refine_Imperative_HOL/IICF/Intf/IICF_Multiset.thy`
The file was modified	`thys/Shadow_DOM/Shadow_DOM.thy`
The file was removed	`thys/Berlekamp_Zassenhaus/Missing_Multiset2.thy`
The file was removed	`thys/PAC_Checker/Duplicate_Free_Multiset.thy`