src/HOL/NumberTheory/Gauss.thy
changeset 29270 0eade173f77e
parent 27556 292098f2efdf
child 30034 60f64f112174