src/HOL/Algebra/Bij.thy
changeset 29270 0eade173f77e
parent 27717 21bbd410ba04
child 31754 b5260f5272a4