src/HOL/Algebra/Bij.thy
changeset 14470 1ffe42cfaefe
parent 13945 5433b2755e98
child 14666 65f8680c3f16