src/HOL/Algebra/Bij.thy
changeset 13949 0ce528cd6f19
parent 13945 5433b2755e98
child 14666 65f8680c3f16