src/HOL/Algebra/Bij.thy
changeset 30562 7b0017587e7d
parent 27717 21bbd410ba04
child 31754 b5260f5272a4