Changes

Summary

more succint formulation of membership for multisets, similar to lists

Changeset 6387:26bbd9a85c0c by haftmann: more succint formulation of membership for multisets, similar to lists
The file was modified	`thys/Algebraic_Numbers/Algebraic_Numbers.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Unique_Factorization_Poly.thy` (diff)
The file was modified	`thys/Amortized_Complexity/Splay_Heap.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Lib/Misc.thy` (diff)
The file was modified	`thys/Binomial-Heaps/SkewBinomialHeap.thy` (diff)
The file was modified	`thys/Collections/ICF/gen_algo/PrioByAnnotatedList.thy` (diff)
The file was modified	`thys/Decreasing-Diagrams-II/Decreasing_Diagrams_II_Aux.thy` (diff)
The file was modified	`thys/Decreasing-Diagrams/Decreasing_Diagrams.thy` (diff)
The file was modified	`thys/LTL_to_GBA/LTL_to_GBA.thy` (diff)
The file was modified	`thys/Landau_Symbols/Group_Sort.thy` (diff)
The file was modified	`thys/Nominal2/Nominal2_Base.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Dvd_Int_Poly.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Missing_Multiset.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Polynomial_Divisibility.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Rational_Factorization.thy` (diff)
The file was modified	`thys/Priority_Queue_Braun/Priority_Queue_Braun.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/ConstraintSystems.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/Misc.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/Normalization.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/Semantics.thy` (diff)
The file was modified	`thys/SATSolverVerification/SatSolverVerification.thy` (diff)
The file was modified	`thys/Selection_Heap_Sort/Heap.thy` (diff)
The file was modified	`thys/Selection_Heap_Sort/RemoveMax.thy` (diff)
The file was modified	`thys/SequentInvertibility/ModalSequents.thy` (diff)
The file was modified	`thys/SequentInvertibility/MultiSequents.thy` (diff)
The file was modified	`thys/SequentInvertibility/NominalSequents.thy` (diff)
The file was modified	`thys/SequentInvertibility/SRCTransforms.thy` (diff)
The file was modified	`thys/SequentInvertibility/SingleSuccedent.thy` (diff)
The file was modified	`thys/Well_Quasi_Orders/Multiset_Extension.thy` (diff)