--- a/src/HOL/Library/Float.thy Wed May 04 11:49:46 2011 +0200
+++ b/src/HOL/Library/Float.thy Wed May 04 15:37:39 2011 +0200
@@ -85,10 +85,10 @@
by (auto simp add: h)
show ?thesis
proof (induct a)
- case (1 n)
+ case (nonneg n)
from pos show ?case by (simp add: algebra_simps)
next
- case (2 n)
+ case (neg n)
show ?case
apply (auto)
apply (subst pow2_neg[of "- int n"])
@@ -100,7 +100,7 @@
lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
proof (induct b)
- case (1 n)
+ case (nonneg n)
show ?case
proof (induct n)
case 0
@@ -110,7 +110,7 @@
then show ?case by (auto simp add: algebra_simps pow2_add1)
qed
next
- case (2 n)
+ case (neg n)
show ?case
proof (induct n)
case 0