changeset 82537 | 3dfd62b4e2c8 |
parent 75804 | dd04e81172a8 |
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Tue Apr 22 15:41:34 2025 +0200 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Tue Apr 22 19:02:33 2025 +0200 @@ -30,6 +30,7 @@ "Gcd :: _ poly set \<Rightarrow> _" "Lcm :: _ poly set \<Rightarrow> _" nlists + Multiset.multisets_of_size ]] text \<open>