src/HOL/Tools/inductive_codegen.ML
changeset 18320 ce523820ff75
parent 17521 0f1c48de39f5
child 18388 ab1a710a68ce