src/HOL/Tools/inductive_codegen.ML
changeset 43962 e1d29c3ca933
parent 43878 eeb10fdd9535
child 44058 ae85c5d64913