src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
changeset 54437 0060957404c7
parent 54295 45a5523d4a63
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sat Nov 16 07:45:53 2013 +0100
     1.2 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Fri Nov 15 22:02:01 2013 +0100
     1.3 @@ -40,6 +40,18 @@
     1.4  lemma [code, code del]:
     1.5    "Cardinality.eq_set = Cardinality.eq_set" ..
     1.6  
     1.7 +lemma [code, code del]:
     1.8 +  "(Gcd :: nat set \<Rightarrow> nat) = Gcd" ..
     1.9 +
    1.10 +lemma [code, code del]:
    1.11 +  "(Lcm :: nat set \<Rightarrow> nat) = Lcm" ..
    1.12 +
    1.13 +lemma [code, code del]:
    1.14 +  "(Gcd :: int set \<Rightarrow> int) = Gcd" ..
    1.15 +
    1.16 +lemma [code, code del]:
    1.17 +  "(Lcm :: int set \<Rightarrow> int) = Lcm" ..
    1.18 +  
    1.19  (*
    1.20    If the code generation ends with an exception with the following message:
    1.21    '"List.set" is not a constructor, on left hand side of equation: ...',