# HG changeset patch
# User nipkow
# Date 1503831733 -7200
# Node ID b48077ae8b1277098444dde5934b6e8c1d2dd8d9
# Parent  b6d04f487ddd68fdfc9c45204e96dca12fa9df92
tuned

diff -r b6d04f487ddd -r b48077ae8b12 src/HOL/Transcendental.thy
--- 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