src/HOL/Tools/datatype_hooks.ML
changeset 23075 69e30a7e8880
parent 22846 fb79144af9a3
child 24305 b1df9e31cda1