src/ZF/func.thy
changeset 25571 c9e39eafc7a0
parent 24893 b8ef7afe3a6b
child 27150 a42aef558ce3