src/HOL/Old_Number_Theory/BijectionRel.thy
changeset 63045 c50c764aab10
parent 61382 efac889fccbc