src/HOL/Algebra/Bij.thy
changeset 69768 7e4966eaf781
parent 68687 2976a4a3b126