src/HOL/NumberTheory/BijectionRel.thy
changeset 12791 ccc0f45ad2c4
parent 11549 e7265e70fd7c
child 13524 604d0f3622d6