src/HOL/Algebra/Bij.thy
changeset 61741 adf6dd1d490e
parent 61382 efac889fccbc
child 63167 0909deb8059b