src/HOL/Recdef.thy
changeset 6811 4700ca722bbd
parent 6438 e55a1869ed38
child 7357 d0e16da40ea2