src/HOL/Tools/datatype_aux.ML
changeset 18418 bf448d999b7e
parent 18377 0e1d025d57b3
child 18728 6790126ab5f6