src/HOL/Tools/list_code.ML
changeset 49972 f11f8905d9fd
parent 48072 ace701efe203
equal deleted inserted replaced
49971:8b50286c36d3 49972:f11f8905d9fd