src/HOL/Algebra/Bij.thy
changeset 63056 9b95ae9ec671
parent 61382 efac889fccbc
child 63167 0909deb8059b