src/HOL/Algebra/Bij.thy
changeset 62098 b1b2834bb493
parent 61382 efac889fccbc
child 63167 0909deb8059b