src/HOL/Tools/recfun_codegen.ML
changeset 24432 d555d941f983
parent 24219 e558fe311376
child 24584 01e83ffa6c54
equal deleted inserted replaced
24431:02d29baa42ff 24432:d555d941f983