src/HOL/NumberTheory/BijectionRel.thy
changeset 13181 dc393bbee6ce
parent 11549 e7265e70fd7c
child 13524 604d0f3622d6