src/HOL/NumberTheory/EulerFermat.thy
changeset 29270 0eade173f77e
parent 27556 292098f2efdf
child 30042 31039ee583fa