src/HOL/Real/Float.thy
changeset 20217 25b068a99d2b
parent 19765 dfe940911617
child 20485 3078fd2eec7b
     1.1 --- a/src/HOL/Real/Float.thy	Wed Jul 26 13:31:07 2006 +0200
     1.2 +++ b/src/HOL/Real/Float.thy	Wed Jul 26 19:23:04 2006 +0200
     1.3 @@ -28,9 +28,7 @@
     1.4      apply (auto, induct_tac n)
     1.5      apply (simp_all add: pow2_def)
     1.6      apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
     1.7 -    apply (auto simp add: h)
     1.8 -    apply arith
     1.9 -    done
    1.10 +    by (auto simp add: h)
    1.11    show ?thesis
    1.12    proof (induct a)
    1.13      case (1 n)