changeset 66521 | b48077ae8b12 |
parent 66515 | 85c505c98332 |
child 66827 | c94531b5007d |
--- 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