src/HOL/Old_Number_Theory/BijectionRel.thy
changeset 61898 6c7861f783fd
parent 61382 efac889fccbc