src/HOL/Number_Theory/Mod_Exp.thy
changeset 82913 7c870287f04f
parent 69790 154cf64e403e