src/HOL/Algebra/Bij.thy
changeset 14213 7bf882b0a51e
parent 13945 5433b2755e98
child 14666 65f8680c3f16