src/HOL/NumberTheory/EulerFermat.thy
changeset 12791 ccc0f45ad2c4
parent 11868 56db9f3a6b3e
child 13187 e5434b822a96