src/HOL/Recdef.thy
changeset 11557 66b62cbeaab3
parent 11533 0c0d2332e8f0
child 12023 d982f98e0f0d