changeset 75804 | dd04e81172a8 |
parent 73886 | 93ba8e3fdcdf |
child 82537 | 3dfd62b4e2c8 |
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Thu Aug 11 10:11:21 2022 +0200 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Thu Aug 11 11:57:19 2022 +0200 @@ -29,6 +29,7 @@ Euclidean_Algorithm.Lcm "Gcd :: _ poly set \<Rightarrow> _" "Lcm :: _ poly set \<Rightarrow> _" + nlists ]] text \<open>