src/HOL/ex/Recdef.thy
changeset 3564 f886dbd91ee5
parent 3418 f060dc3f15a8
child 3590 4d307341d0af