src/HOL/Tools/inductive_codegen.ML
changeset 18067 8b9848d150ba
parent 17521 0f1c48de39f5
child 18388 ab1a710a68ce