src/HOL/Tools/recfun_codegen.ML
changeset 20192 956cd30ef3be
parent 19788 be3a84d22a58
child 20597 65fe827aa595