src/HOL/NumberTheory/Quadratic_Reciprocity.thy
changeset 15911 b730b0edc085
parent 15541 206d779ba96d
child 16663 13e9c402308b