src/HOL/Algebra/Bij.thy
changeset 79705 a6dc0d4ffea2
parent 68687 2976a4a3b126