src/HOL/List.ML
changeset 974 68d58134fad6
parent 962 136308504cd9
child 995 95c148a7b9c4
equal deleted inserted replaced
973:f57fb576520f 974:68d58134fad6
    35    append_Nil, append_Cons,
    35    append_Nil, append_Cons,
    36    map_Nil, map_Cons,
    36    map_Nil, map_Cons,
    37    flat_Nil, flat_Cons,
    37    flat_Nil, flat_Cons,
    38    list_all_Nil, list_all_Cons,
    38    list_all_Nil, list_all_Cons,
    39    filter_Nil, filter_Cons,
    39    filter_Nil, filter_Cons,
       
    40    foldl_Nil, foldl_Cons,
    40    length_Nil, length_Cons];
    41    length_Nil, length_Cons];
    41 
    42 
    42 
    43 
    43 (** @ - append **)
    44 (** @ - append **)
    44 
    45