src/ZF/func.thy
changeset 27187 17b63e145986
parent 27150 a42aef558ce3
child 27702 80608e96e760