src/ZF/func.thy
changeset 8141 d6d896e81cd7
parent 2469 b50b8c0eec01
child 13163 e320a52ff711