src/HOL/Tools/datatype_codegen.ML
changeset 23075 69e30a7e8880
parent 22921 475ff421a6a3
child 23513 2ebb50c0db4f