src/HOL/Tools/datatype_hooks.ML
changeset 21513 9e9fff87dc6c
parent 21251 94e77628a47d
child 22846 fb79144af9a3