src/HOL/Algebra/Bij.thy
changeset 31409 d8537ba165b5
parent 27717 21bbd410ba04
child 31754 b5260f5272a4