src/HOL/Recdef.thy
changeset 38859 053c69cb4a0e
parent 38554 f8999e19dd49
child 39198 f967a16dfcdd