src/HOL/NumberTheory/EulerFermat.thy
changeset 17401 9147c880ada6
parent 16733 236dfafbeb63
child 18369 694ea14ab4f2