src/HOL/Algebra/Bij.thy
changeset 62540 f2fc5485e3b0
parent 61382 efac889fccbc
child 63167 0909deb8059b