tuned

--- a/src/HOL/Transcendental.thy	Sat Aug 26 23:58:03 2017 +0100
+++ b/src/HOL/Transcendental.thy	Sun Aug 27 13:02:13 2017 +0200
@@ -2773,10 +2773,6 @@
   with assms show ?thesis by(simp add: ceiling_log_nat_eq_powr_iff)
 qed
 
-(* FIXME: a more appropriate place for these two lemmas
-   is a theory of discrete logarithms
-*)
-
 lemma floor_log2_div2: fixes n :: nat assumes "n \<ge> 2"
 shows "floor(log 2 n) = floor(log 2 (n div 2)) + 1"
 proof cases