src/HOL/Tools/inductive_codegen.ML
changeset 31816 ffaf6dd53045
parent 31784 bd3486c57ba3
child 31852 a16bb835e97d