--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Sat Nov 16 07:45:53 2013 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Fri Nov 15 22:02:01 2013 +0100
@@ -40,6 +40,18 @@
lemma [code, code del]:
"Cardinality.eq_set = Cardinality.eq_set" ..
+lemma [code, code del]:
+ "(Gcd :: nat set \<Rightarrow> nat) = Gcd" ..
+
+lemma [code, code del]:
+ "(Lcm :: nat set \<Rightarrow> nat) = Lcm" ..
+
+lemma [code, code del]:
+ "(Gcd :: int set \<Rightarrow> int) = Gcd" ..
+
+lemma [code, code del]:
+ "(Lcm :: int set \<Rightarrow> int) = Lcm" ..
+
(*
If the code generation ends with an exception with the following message:
'"List.set" is not a constructor, on left hand side of equation: ...',