src/HOL/Recdef.thy
changeset 10706 f02834001fca
parent 10653 55f33da63366
child 10773 0deff0197496