doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML
changeset 22015 12b94d7f7e1f
parent 21994 dfa5133dbe73
child 22188 a63889770d57
equal deleted inserted replaced
22014:4b70cbd96007 22015:12b94d7f7e1f
    11 
    11 
    12 structure List = 
    12 structure List = 
    13 struct
    13 struct
    14 
    14 
    15 fun memberl (A_:'a Code_Generator.eq) x (y :: ys) =
    15 fun memberl (A_:'a Code_Generator.eq) x (y :: ys) =
    16   (Code_Generator.op_eq A_ x y orelse memberl A_ x ys)
    16   Code_Generator.op_eq A_ x y orelse memberl A_ x ys
    17   | memberl (A_:'a Code_Generator.eq) x [] = false;
    17   | memberl (A_:'a Code_Generator.eq) x [] = false;
    18 
    18 
    19 end; (*struct List*)
    19 end; (*struct List*)
    20 
    20 
    21 structure Codegen = 
    21 structure Codegen =