--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Wed Mar 24 21:17:19 2021 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Thu Mar 25 08:52:15 2021 +0000
@@ -29,17 +29,15 @@
Euclidean_Algorithm.Lcm
"Gcd :: _ poly set \<Rightarrow> _"
"Lcm :: _ poly set \<Rightarrow> _"
- permutations_of_set
- permutations_of_multiset
]]
text \<open>
If code generation fails with a message like
\<open>"List.set" is not a constructor, on left hand side of equation: ...\<close>,
- feel free to add an RBT implementation for the corrsponding operation
- of delete that code equation (see above).
+ feel free to add an RBT implementation for the corresponding operation
+ or delete that code equation (see above).
\<close>
-
+
export_code _ checking SML OCaml? Haskell? Scala
end