src/HOL/NumberTheory/BijectionRel.thy
changeset 25289 3d332d8a827c
parent 23755 1c4672d130b1