src/HOL/Tools/inductive_codegen.ML
changeset 43928 24d6e759753f
parent 43878 eeb10fdd9535
child 44058 ae85c5d64913