src/HOL/NumberTheory/BijectionRel.thy
changeset 19404 9bf2cdc9e8e8
parent 18369 694ea14ab4f2
child 19670 2e4a143c73c5