src/HOL/Tools/recfun_codegen.ML
changeset 16240 95cc0e8f8a17
parent 15700 970e0293dfb3
child 16424 18a07ad8fea8