Summary
- msetsum/prod -> set/prod_mset
The file was modified | thys/Polynomial_Factorization/Missing_Multiset.thy (diff) |
The file was modified | thys/Polynomial_Factorization/Prime_Factorization.thy (diff) |
The file was modified | thys/Polynomial_Factorization/Missing_Multiset.thy (diff) |
The file was modified | thys/Polynomial_Factorization/Prime_Factorization.thy (diff) |