author | paulson |
Tue, 22 Apr 2025 22:06:52 +0100 | |
changeset 82540 | ad31be996dcb |
parent 82537 | 3dfd62b4e2c8 (diff) |
parent 82539 | fadbfb9e65f3 (current diff) |
child 82541 | 5160b68e78a9 |
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Tue Apr 22 17:35:13 2025 +0100 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Tue Apr 22 22:06:52 2025 +0100 @@ -30,6 +30,7 @@ "Gcd :: _ poly set \<Rightarrow> _" "Lcm :: _ poly set \<Rightarrow> _" nlists + Multiset.multisets_of_size ]] text \<open>