src/HOL/Tools/inductive_codegen.ML
changeset 17970 a84ac7c201ea
parent 17521 0f1c48de39f5
child 18388 ab1a710a68ce