src/HOL/Recdef.thy
changeset 10569 e8346dad78e1
parent 10212 33fe2d701ddd
child 10653 55f33da63366