src/HOL/Library/Float.thy
changeset 42676 8724f20bf69c
parent 41528 276078f01ada
child 44766 d4d33a4d7548
     1.1 --- a/src/HOL/Library/Float.thy	Wed May 04 11:49:46 2011 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Wed May 04 15:37:39 2011 +0200
     1.3 @@ -85,10 +85,10 @@
     1.4      by (auto simp add: h)
     1.5    show ?thesis
     1.6    proof (induct a)
     1.7 -    case (1 n)
     1.8 +    case (nonneg n)
     1.9      from pos show ?case by (simp add: algebra_simps)
    1.10    next
    1.11 -    case (2 n)
    1.12 +    case (neg n)
    1.13      show ?case
    1.14        apply (auto)
    1.15        apply (subst pow2_neg[of "- int n"])
    1.16 @@ -100,7 +100,7 @@
    1.17  
    1.18  lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
    1.19  proof (induct b)
    1.20 -  case (1 n)
    1.21 +  case (nonneg n)
    1.22    show ?case
    1.23    proof (induct n)
    1.24      case 0
    1.25 @@ -110,7 +110,7 @@
    1.26      then show ?case by (auto simp add: algebra_simps pow2_add1)
    1.27    qed
    1.28  next
    1.29 -  case (2 n)
    1.30 +  case (neg n)
    1.31    show ?case
    1.32    proof (induct n)
    1.33      case 0