src/HOL/ex/Recdef.thy
changeset 4571 6b02fc8a97f6
parent 4100 9f6907c40442
child 4606 73227403d497