src/HOL/Tools/datatype_codegen.ML
changeset 21070 0a898140fea2
parent 21046 fe1db2f991a7
child 21454 a1937c51ed88