src/HOL/Recdef.thy
changeset 10355 aef4f587a0e4
parent 10212 33fe2d701ddd
child 10653 55f33da63366