src/HOL/Algebra/Bij.thy
changeset 14024 213dcc39358f
parent 13945 5433b2755e98
child 14666 65f8680c3f16