src/HOL/Tools/recfun_codegen.ML
changeset 20276 d94dc40673b1
parent 19788 be3a84d22a58
child 20597 65fe827aa595
equal deleted inserted replaced
20275:f82435d180ef 20276:d94dc40673b1