src/HOL/Algebra/Bij.thy
changeset 63045 c50c764aab10
parent 61382 efac889fccbc
child 63167 0909deb8059b