src/HOL/Library/Discrete.thy
2013-02-17 haftmann 2013-02-17 fundamentals about discrete logarithm and square root