src/HOL/Algebra/Bij.thy
changeset 30729 461ee3e49ad3
parent 27717 21bbd410ba04
child 31754 b5260f5272a4