src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
changeset 54295 45a5523d4a63
parent 53361 1cb7d3c0cf31
child 54437 0060957404c7
     1.1 --- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sun Nov 10 10:02:34 2013 +0100
     1.2 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sun Nov 10 15:05:06 2013 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4    "pred_of_set = pred_of_set" ..
     1.5  
     1.6  lemma [code, code del]:
     1.7 -  "acc = acc" ..
     1.8 +  "Wellfounded.acc = Wellfounded.acc" ..
     1.9  
    1.10  lemma [code, code del]:
    1.11    "Cardinality.card' = Cardinality.card'" ..