src/HOL/ex/Recdefs.thy
changeset 15216 2fac1f11b7f6
parent 14953 27decf8d40ff
child 16417 9bc16273c2d4