src/HOL/ex/Recdef.thy
changeset 4153 e534c4c32d54
parent 4100 9f6907c40442
child 4606 73227403d497