src/HOL/Tools/inductive_codegen.ML
changeset 17740 fc385ce6187d
parent 17521 0f1c48de39f5
child 18388 ab1a710a68ce