src/HOL/Tools/recdef_package.ML
changeset 15151 429666b09783
parent 15032 02aed07e01bf
child 15458 9c292e3e0ca1