src/HOL/Tools/recdef_package.ML
changeset 21111 624ed9c7c4fe
parent 21098 d0d8a48ae4e6
child 21351 1fb804b96d7c